Split morphisms in an idempotent-complete preadditive category #

This file constructs the complementary summand of a split monomorphism, and dually of a split epimorphism, directly by splitting the complementary idempotent. No kernel or cokernel is assumed.

source

structure QuotientSubmoduleEquidistribution.SplitMonoComplement {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsSplitMono f] :

Type (max u v)

A splitting of the idempotent complementary to a split monomorphism.

complement : C
The complementary object.
inclusion : self.complement ⟶ Y
Inclusion of the complementary object.
projection : Y ⟶ self.complement
Projection onto the complementary object.
inclusion_projection : CategoryTheory.CategoryStruct.comp self.inclusion self.projection = CategoryTheory.CategoryStruct.id self.complement
projection_inclusion : CategoryTheory.CategoryStruct.comp self.projection self.inclusion = CategoryTheory.CategoryStruct.id Y - CategoryTheory.CategoryStruct.comp (CategoryTheory.retraction f) f

Instances For

source

noncomputable def QuotientSubmoduleEquidistribution.splitMonoComplement {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsSplitMono f] [CategoryTheory.IsIdempotentComplete C] :

SplitMonoComplement f

An idempotent-complete preadditive category supplies a complement to every split monomorphism, by splitting 𝟙 Y - retraction f ≫ f.

Instances For

source

@[simp]

theorem QuotientSubmoduleEquidistribution.SplitMonoComplement.f_projection {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [hf : CategoryTheory.IsSplitMono f] (d : SplitMonoComplement f) :

CategoryTheory.CategoryStruct.comp f d.projection = 0

source

@[simp]

theorem QuotientSubmoduleEquidistribution.SplitMonoComplement.f_projection_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [hf : CategoryTheory.IsSplitMono f] (d : SplitMonoComplement f) {Z : C} (h : d.complement ⟶ Z) :

CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp d.projection h) = CategoryTheory.CategoryStruct.comp 0 h

source

@[simp]

theorem QuotientSubmoduleEquidistribution.SplitMonoComplement.inclusion_retraction {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [hf : CategoryTheory.IsSplitMono f] (d : SplitMonoComplement f) :

CategoryTheory.CategoryStruct.comp d.inclusion (CategoryTheory.retraction f) = 0

source

@[simp]

theorem QuotientSubmoduleEquidistribution.SplitMonoComplement.inclusion_retraction_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [hf : CategoryTheory.IsSplitMono f] (d : SplitMonoComplement f) {Z : C} (h : X ⟶ Z) :

CategoryTheory.CategoryStruct.comp d.inclusion (CategoryTheory.CategoryStruct.comp (CategoryTheory.retraction f) h) = CategoryTheory.CategoryStruct.comp 0 h

source

theorem QuotientSubmoduleEquidistribution.SplitMonoComplement.total {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [hf : CategoryTheory.IsSplitMono f] (d : SplitMonoComplement f) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.retraction f) f + CategoryTheory.CategoryStruct.comp d.projection d.inclusion = CategoryTheory.CategoryStruct.id Y

source

noncomputable def QuotientSubmoduleEquidistribution.SplitMonoComplement.binaryBicone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [hf : CategoryTheory.IsSplitMono f] (d : SplitMonoComplement f) :

CategoryTheory.Limits.BinaryBicone X d.complement

The chosen ambient object Y as the biproduct of the source and the complement.

Instances For

source

@[simp]

theorem QuotientSubmoduleEquidistribution.SplitMonoComplement.binaryBicone_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [hf : CategoryTheory.IsSplitMono f] (d : SplitMonoComplement f) :

d.binaryBicone.fst = CategoryTheory.retraction f

source

@[simp]

theorem QuotientSubmoduleEquidistribution.SplitMonoComplement.binaryBicone_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [hf : CategoryTheory.IsSplitMono f] (d : SplitMonoComplement f) :

d.binaryBicone.snd = d.projection

source

@[simp]

theorem QuotientSubmoduleEquidistribution.SplitMonoComplement.binaryBicone_inl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [hf : CategoryTheory.IsSplitMono f] (d : SplitMonoComplement f) :

d.binaryBicone.inl = f

source

@[simp]

theorem QuotientSubmoduleEquidistribution.SplitMonoComplement.binaryBicone_inr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [hf : CategoryTheory.IsSplitMono f] (d : SplitMonoComplement f) :

d.binaryBicone.inr = d.inclusion

source

@[simp]

theorem QuotientSubmoduleEquidistribution.SplitMonoComplement.binaryBicone_pt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [hf : CategoryTheory.IsSplitMono f] (d : SplitMonoComplement f) :

d.binaryBicone.pt = Y

source

noncomputable def QuotientSubmoduleEquidistribution.SplitMonoComplement.isBilimitBinaryBicone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [hf : CategoryTheory.IsSplitMono f] (d : SplitMonoComplement f) :

d.binaryBicone.IsBilimit

The preceding bicone is a genuine binary biproduct, without assuming that the category has binary biproducts globally.

Instances For

source

def QuotientSubmoduleEquidistribution.SplitMonoComplement.shortComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [hf : CategoryTheory.IsSplitMono f] (d : SplitMonoComplement f) :

CategoryTheory.ShortComplex C

The split short complex X → Y → complement attached to a split monomorphism.

Instances For

source

noncomputable def QuotientSubmoduleEquidistribution.SplitMonoComplement.splitting {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [hf : CategoryTheory.IsSplitMono f] (d : SplitMonoComplement f) :

d.shortComplex.Splitting

The complement data give Mathlib's native short-complex splitting.

Instances For

source

structure QuotientSubmoduleEquidistribution.SplitEpiComplement {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (g : X ⟶ Y) [CategoryTheory.IsSplitEpi g] :

Type (max u v)

A splitting of the idempotent complementary to a split epimorphism.

complement : C
The complementary object.
inclusion : self.complement ⟶ X
Inclusion of the complementary object.
projection : X ⟶ self.complement
Projection onto the complementary object.
inclusion_projection : CategoryTheory.CategoryStruct.comp self.inclusion self.projection = CategoryTheory.CategoryStruct.id self.complement
projection_inclusion : CategoryTheory.CategoryStruct.comp self.projection self.inclusion = CategoryTheory.CategoryStruct.id X - CategoryTheory.CategoryStruct.comp g (CategoryTheory.section_ g)

Instances For

source

noncomputable def QuotientSubmoduleEquidistribution.splitEpiComplement {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (g : X ⟶ Y) [CategoryTheory.IsSplitEpi g] [CategoryTheory.IsIdempotentComplete C] :

SplitEpiComplement g

An idempotent-complete preadditive category supplies a complement to every split epimorphism, by splitting 𝟙 X - g ≫ section_ g.

Instances For

source

@[simp]

theorem QuotientSubmoduleEquidistribution.SplitEpiComplement.section_projection {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {g : X ⟶ Y} [hg : CategoryTheory.IsSplitEpi g] (d : SplitEpiComplement g) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.section_ g) d.projection = 0

source

@[simp]

theorem QuotientSubmoduleEquidistribution.SplitEpiComplement.section_projection_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {g : X ⟶ Y} [hg : CategoryTheory.IsSplitEpi g] (d : SplitEpiComplement g) {Z : C} (h : d.complement ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.section_ g) (CategoryTheory.CategoryStruct.comp d.projection h) = CategoryTheory.CategoryStruct.comp 0 h

source

@[simp]

theorem QuotientSubmoduleEquidistribution.SplitEpiComplement.inclusion_g {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {g : X ⟶ Y} [hg : CategoryTheory.IsSplitEpi g] (d : SplitEpiComplement g) :

CategoryTheory.CategoryStruct.comp d.inclusion g = 0

source

@[simp]

theorem QuotientSubmoduleEquidistribution.SplitEpiComplement.inclusion_g_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {g : X ⟶ Y} [hg : CategoryTheory.IsSplitEpi g] (d : SplitEpiComplement g) {Z : C} (h : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp d.inclusion (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp 0 h

source

theorem QuotientSubmoduleEquidistribution.SplitEpiComplement.total {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {g : X ⟶ Y} [hg : CategoryTheory.IsSplitEpi g] (d : SplitEpiComplement g) :

CategoryTheory.CategoryStruct.comp d.projection d.inclusion + CategoryTheory.CategoryStruct.comp g (CategoryTheory.section_ g) = CategoryTheory.CategoryStruct.id X

source

noncomputable def QuotientSubmoduleEquidistribution.SplitEpiComplement.binaryBicone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {g : X ⟶ Y} [hg : CategoryTheory.IsSplitEpi g] (d : SplitEpiComplement g) :

CategoryTheory.Limits.BinaryBicone d.complement Y

The chosen ambient object X as the biproduct of the complement and the target.

Instances For

source

@[simp]

theorem QuotientSubmoduleEquidistribution.SplitEpiComplement.binaryBicone_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {g : X ⟶ Y} [hg : CategoryTheory.IsSplitEpi g] (d : SplitEpiComplement g) :

d.binaryBicone.snd = g

source

@[simp]

theorem QuotientSubmoduleEquidistribution.SplitEpiComplement.binaryBicone_inr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {g : X ⟶ Y} [hg : CategoryTheory.IsSplitEpi g] (d : SplitEpiComplement g) :

d.binaryBicone.inr = CategoryTheory.section_ g

source

@[simp]

theorem QuotientSubmoduleEquidistribution.SplitEpiComplement.binaryBicone_pt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {g : X ⟶ Y} [hg : CategoryTheory.IsSplitEpi g] (d : SplitEpiComplement g) :

d.binaryBicone.pt = X

source

@[simp]

theorem QuotientSubmoduleEquidistribution.SplitEpiComplement.binaryBicone_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {g : X ⟶ Y} [hg : CategoryTheory.IsSplitEpi g] (d : SplitEpiComplement g) :

d.binaryBicone.fst = d.projection

source

@[simp]

theorem QuotientSubmoduleEquidistribution.SplitEpiComplement.binaryBicone_inl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {g : X ⟶ Y} [hg : CategoryTheory.IsSplitEpi g] (d : SplitEpiComplement g) :

d.binaryBicone.inl = d.inclusion

source

noncomputable def QuotientSubmoduleEquidistribution.SplitEpiComplement.isBilimitBinaryBicone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {g : X ⟶ Y} [hg : CategoryTheory.IsSplitEpi g] (d : SplitEpiComplement g) :

d.binaryBicone.IsBilimit

The preceding bicone is a genuine binary biproduct, without assuming that the category has binary biproducts globally.

Instances For

source

def QuotientSubmoduleEquidistribution.SplitEpiComplement.shortComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {g : X ⟶ Y} [hg : CategoryTheory.IsSplitEpi g] (d : SplitEpiComplement g) :

CategoryTheory.ShortComplex C

The split short complex complement → X → Y attached to a split epimorphism.

Instances For

source

noncomputable def QuotientSubmoduleEquidistribution.SplitEpiComplement.splitting {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {g : X ⟶ Y} [hg : CategoryTheory.IsSplitEpi g] (d : SplitEpiComplement g) :

d.shortComplex.Splitting

The complement data give Mathlib's native short-complex splitting.

Instances For

Magnitude conjecture

QuotientSubmoduleEquidistribution.CategoryTheory.SplitMorphismComplement

Split morphisms in an idempotent-complete preadditive category #