Linear two-sided Hom ideals generated by relations

This file constructs the Hom ideal linearly generated by a family of categorical relations and equips its categorical quotient with the inherited linear structure.

def QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.linearSpan_hom {K : Type w} {C : Type u} [Ring K] [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [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 QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.relation_mem_linearSpan {K : Type w} {C : Type u} [Ring K] [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [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 QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.composite_mem_linearSpan {K : Type w} {C : Type u} [Ring K] [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [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 QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.smul_mem {K : Type w} {C : Type u} [Ring K] [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [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 QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.linearSpan_le {K : Type w} {C : Type u} [Ring K] [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [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 QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.linearSpan_le_iff {K : Type w} {C : Type u} [Ring K] [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [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 QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.rel_smul_compatible {K : Type w} {C : Type u} [Ring K] [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [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 QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.quotientLinear {K : Type w} {C : Type u} [Ring K] [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [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 QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.quotientFunctorLinear {K : Type w} {C : Type u} [Ring K] [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [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.