Two-sided Hom ideals and their linear quotients

A two-sided additive ideal of morphisms in a preadditive category, the quotient category it defines, and the ideal linearly generated by a family of relations. These are generic foundations; the scalar mesh categories of Definition 2.4 are quotients of this form.

Borrowed from the magnitude-conjecture formalization, files QuotientSubmoduleEquidistribution/CategoryTheory/{HomIdeal,IdealQuotient, LinearGeneratedHomIdeal}.lean (last changed at commit 2659d1755), with the namespace changed, the radical-morphism lemmas omitted, and no change of statements or proofs.

structure MultiplicativeBasisDeformations.CategoricalIdeal.HomIdeal (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : Type (max u v)

A two-sided additive ideal in a preadditive category.

• hom (X Y : C) : AddSubgroup (X ⟶ Y)
• precomp {X Y Z : C} (f : X ⟶ Y) {g : Y ⟶ Z} : g ∈ self.hom Y Z → CategoryTheory.CategoryStruct.comp f g ∈ self.hom X Z
• postcomp {X Y Z : C} {f : X ⟶ Y} (g : Y ⟶ Z) : f ∈ self.hom X Y → CategoryTheory.CategoryStruct.comp f g ∈ self.hom X Z

def MultiplicativeBasisDeformations.CategoricalIdeal.HomIdeal.rel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) : HomRel C

Congruence modulo the given Hom ideal.

instance MultiplicativeBasisDeformations.CategoricalIdeal.HomIdeal.instCongruenceRel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) : CategoryTheory.Congruence I.rel

theorem MultiplicativeBasisDeformations.CategoricalIdeal.HomIdeal.add_compatible {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) {X Y : C} (f₁ f₂ g₁ g₂ : X ⟶ Y) (hf : I.rel f₁ f₂) (hg : I.rel g₁ g₂) : I.rel (f₁ + g₁) (f₂ + g₂)

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.CategoricalIdeal.HomIdeal.quotientPreadditive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) : CategoryTheory.Preadditive (CategoryTheory.Quotient I.rel)

The induced preadditive structure on the category quotient.

theorem MultiplicativeBasisDeformations.CategoricalIdeal.HomIdeal.map_eq_zero_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Quotient.functor I.rel).map f = 0 ↔ f ∈ I.hom X Y

The quotient functor kills exactly the given Hom ideal.

def MultiplicativeBasisDeformations.CategoricalIdeal.HomIdeal.twoSidedCompositeSet {C : Type u} [CategoryTheory.Category.{v, u} C] (R : (X Y : C) → Set (X ⟶ Y)) (X Y : C) : Set (X ⟶ Y)

Morphisms obtained by composing a specified relation on both sides.

def MultiplicativeBasisDeformations.CategoricalIdeal.HomIdeal.generatedHomSubmodule {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (𝕜 : Type w) [Ring 𝕜] [CategoryTheory.Linear 𝕜 C] (R : (X Y : C) → Set (X ⟶ Y)) (X Y : C) : Submodule 𝕜 (X ⟶ Y)

The linear span of all two-sided composites through a relation generator.

def MultiplicativeBasisDeformations.CategoricalIdeal.HomIdeal.linearSpan {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (𝕜 : Type w) [Ring 𝕜] [CategoryTheory.Linear 𝕜 C] (R : (X Y : C) → Set (X ⟶ Y)) : HomIdeal C

The two-sided additive Hom ideal linearly generated by R.

@[simp]

theorem MultiplicativeBasisDeformations.CategoricalIdeal.HomIdeal.linearSpan_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : Type w} [Ring K] [CategoryTheory.Linear K C] (R : (X Y : C) → Set (X ⟶ Y)) (X Y : C) : (linearSpan K R).hom X Y = (generatedHomSubmodule K R X Y).toAddSubgroup

theorem MultiplicativeBasisDeformations.CategoricalIdeal.HomIdeal.relation_mem_linearSpan {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : Type w} [Ring K] [CategoryTheory.Linear K C] (R : (X Y : C) → Set (X ⟶ Y)) {X Y : C} {r : X ⟶ Y} (hr : r ∈ R X Y) : r ∈ (linearSpan K R).hom X Y

Every specified relation belongs to its generated Hom ideal.

theorem MultiplicativeBasisDeformations.CategoricalIdeal.HomIdeal.composite_mem_linearSpan {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : Type w} [Ring K] [CategoryTheory.Linear K C] (R : (X Y : C) → Set (X ⟶ Y)) {X Y A B : C} (a : X ⟶ A) {r : A ⟶ B} (hr : r ∈ R A B) (b : B ⟶ Y) : CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp r b) ∈ (linearSpan K R).hom X Y

Every two-sided composite through a relation belongs to the generated ideal.

theorem MultiplicativeBasisDeformations.CategoricalIdeal.HomIdeal.smul_mem {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : Type w} [Ring K] [CategoryTheory.Linear K C] (I : HomIdeal C) {X Y : C} (k : K) {f : X ⟶ Y} (hf : f ∈ I.hom X Y) : k • f ∈ I.hom X Y

A Hom ideal in a linear category is automatically closed under scalars.

theorem MultiplicativeBasisDeformations.CategoricalIdeal.HomIdeal.linearSpan_le {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : Type w} [Ring K] [CategoryTheory.Linear K C] (R : (X Y : C) → Set (X ⟶ Y)) (I : HomIdeal C) (hR : ∀ {X Y : C} {r : X ⟶ Y}, r ∈ R X Y → r ∈ I.hom X Y) {X Y : C} {f : X ⟶ Y} : f ∈ (linearSpan K R).hom X Y → f ∈ I.hom X Y

Minimality of the linearly generated Hom ideal.

theorem MultiplicativeBasisDeformations.CategoricalIdeal.HomIdeal.linearSpan_le_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : Type w} [Ring K] [CategoryTheory.Linear K C] (R : (X Y : C) → Set (X ⟶ Y)) (I : HomIdeal C) : (∀ {X Y : C} {f : X ⟶ Y}, f ∈ (linearSpan K R).hom X Y → f ∈ I.hom X Y) ↔ ∀ {X Y : C} {r : X ⟶ Y}, r ∈ R X Y → r ∈ I.hom X Y

Universal property of the generated ideal.

theorem MultiplicativeBasisDeformations.CategoricalIdeal.HomIdeal.rel_smul_compatible {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : Type w} [Ring K] [CategoryTheory.Linear K C] (I : HomIdeal C) (k : K) {X Y : C} (f g : X ⟶ Y) (hfg : I.rel f g) : I.rel (k • f) (k • g)

Congruence modulo a Hom ideal is compatible with scalar multiplication.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.CategoricalIdeal.HomIdeal.quotientLinear {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : Type w} [Ring K] [CategoryTheory.Linear K C] (I : HomIdeal C) : CategoryTheory.Linear K (CategoryTheory.Quotient I.rel)

The induced linear structure on a Hom-ideal quotient.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.CategoricalIdeal.HomIdeal.quotientFunctorLinear {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : Type w} [Ring K] [CategoryTheory.Linear K C] (I : HomIdeal C) : CategoryTheory.Functor.Linear K (CategoryTheory.Quotient.functor I.rel)

The quotient functor is linear for the induced quotient structure.