Linear functors out of Hom-ideal quotients

An additive linear functor which kills a two-sided Hom ideal factors through the corresponding categorical quotient. Fullness descends to the quotient, while the reverse inclusion from the functor kernel into the Hom ideal makes the descended functor faithful.

This is the representation-independent quotient-realization kernel migrated from the Cartan formalization.

@[instance_reducible]

def QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.quotientPreadditiveInstance {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) : CategoryTheory.Preadditive (CategoryTheory.Quotient I.rel)

@[instance_reducible]

def QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.quotientLinearInstance {k : Type w} [Ring k] {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (I : HomIdeal C) : CategoryTheory.Linear k (CategoryTheory.Quotient I.rel)

def QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.functorKernel {k : Type w} [Ring k] {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] : HomIdeal C

The two-sided Hom ideal consisting of the morphisms killed by a linear functor.

@[simp]

theorem QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.mem_functorKernel_iff {k : Type w} [Ring k] {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] {X Y : C} (f : X ⟶ Y) : f ∈ (functorKernel F).hom X Y ↔ F.map f = 0

def QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.IsKilledBy {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] (I : HomIdeal C) (F : CategoryTheory.Functor C D) : Prop

An additive functor kills a Hom ideal when every member of the ideal maps to zero.

theorem QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.map_eq_of_rel {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] (I : HomIdeal C) (F : CategoryTheory.Functor C D) [F.Additive] (hI : I.IsKilledBy F) {X Y : C} (f g : X ⟶ Y) (hfg : I.rel f g) : F.map f = F.map g

A functor which kills a Hom ideal respects congruence modulo that ideal.

def QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.quotientLift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] (I : HomIdeal C) (F : CategoryTheory.Functor C D) [F.Additive] (hI : I.IsKilledBy F) : CategoryTheory.Functor (CategoryTheory.Quotient I.rel) D

The functor induced on the quotient by a killed Hom ideal.

def QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.quotientLiftNatTrans {k : Type w} [Ring k] {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (I : HomIdeal C) (F : CategoryTheory.Functor C D) [F.Additive] {G : CategoryTheory.Functor C D} [G.Additive] [CategoryTheory.Functor.Linear k G] (hF : I.IsKilledBy F) (hG : I.IsKilledBy G) (α : F ⟶ G) : I.quotientLift F ⋯ ⟶ I.quotientLift G ⋯

A natural transformation between functors killing the same Hom ideal descends componentwise to their quotient lifts.

def QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.quotientLiftNatIso {k : Type w} [Ring k] {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (I : HomIdeal C) (F : CategoryTheory.Functor C D) [F.Additive] {G : CategoryTheory.Functor C D} [G.Additive] [CategoryTheory.Functor.Linear k G] (hF : I.IsKilledBy F) (hG : I.IsKilledBy G) (α : F ≅ G) : I.quotientLift F ⋯ ≅ I.quotientLift G ⋯

A natural isomorphism between functors killing the same Hom ideal descends componentwise to their quotient lifts.

@[simp]

theorem QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.quotientLift_map_functor_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] (I : HomIdeal C) (F : CategoryTheory.Functor C D) [F.Additive] (hI : I.IsKilledBy F) {X Y : C} (f : X ⟶ Y) : (I.quotientLift F ⋯).map ((CategoryTheory.Quotient.functor I.rel).map f) = F.map f

instance QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.quotientLift_additive {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] (I : HomIdeal C) (F : CategoryTheory.Functor C D) [F.Additive] (hI : I.IsKilledBy F) : (I.quotientLift F ⋯).Additive

instance QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.quotientLift_linear {k : Type w} [Ring k] {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (I : HomIdeal C) (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] (hI : I.IsKilledBy F) : CategoryTheory.Functor.Linear k (I.quotientLift F ⋯)

instance QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.quotientLift_full {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] (I : HomIdeal C) (F : CategoryTheory.Functor C D) [F.Additive] (hI : I.IsKilledBy F) [F.Full] : (I.quotientLift F ⋯).Full

theorem QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.quotientLift_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] (I : HomIdeal C) (F : CategoryTheory.Functor C D) [F.Additive] (hI : I.IsKilledBy F) (hker : ∀ {X Y : C} {f : X ⟶ Y}, F.map f = 0 → f ∈ I.hom X Y) : (I.quotientLift F ⋯).Faithful

If every morphism killed by the original functor already belongs to the quotient ideal, the descended functor is faithful.