Module docstring
{"# Facts about epimorphisms and monomorphisms.
The definitions of Epi and Mono are in CategoryTheory.Category,
since they are used by some lemmas for Iso, which is used everywhere.
"}
CategoryTheory.unop_mono_of_epi
instance
{A B : Cᵒᵖ} (f : A ⟶ B) [Epi f] : Mono f.unop
Full source
instance unop_mono_of_epi {A B : Cᵒᵖ} (f : A ⟶ B) [Epi f] : Mono f.unop :=
⟨fun _ _ eq => Quiver.Hom.op_inj ((cancel_epi f).1 (Quiver.Hom.unop_inj eq))⟩Informal description
For any morphism $f : A \to B$ in the opposite category $C^{\mathrm{op}}$, if $f$ is an epimorphism, then its underlying morphism $\mathrm{unop}(f) : \mathrm{unop}(B) \to \mathrm{unop}(A)$ in $C$ is a monomorphism.
CategoryTheory.unop_epi_of_mono
instance
{A B : Cᵒᵖ} (f : A ⟶ B) [Mono f] : Epi f.unop
Full source
instance unop_epi_of_mono {A B : Cᵒᵖ} (f : A ⟶ B) [Mono f] : Epi f.unop :=
⟨fun _ _ eq => Quiver.Hom.op_inj ((cancel_mono f).1 (Quiver.Hom.unop_inj eq))⟩Informal description
For any morphism $f : A \to B$ in the opposite category $C^{\mathrm{op}}$, if $f$ is a monomorphism, then its underlying morphism $\mathrm{unop}(f) : \mathrm{unop}(B) \to \mathrm{unop}(A)$ in $C$ is an epimorphism.
CategoryTheory.op_mono_of_epi
instance
{A B : C} (f : A ⟶ B) [Epi f] : Mono f.op
Full source
instance op_mono_of_epi {A B : C} (f : A ⟶ B) [Epi f] : Mono f.op :=
⟨fun _ _ eq => Quiver.Hom.unop_inj ((cancel_epi f).1 (Quiver.Hom.op_inj eq))⟩Informal description
For any epimorphism $f : A \to B$ in a category $C$, the opposite morphism $f^{\mathrm{op}} : B^{\mathrm{op}} \to A^{\mathrm{op}}$ in the opposite category $C^{\mathrm{op}}$ is a monomorphism.
CategoryTheory.op_epi_of_mono
instance
{A B : C} (f : A ⟶ B) [Mono f] : Epi f.op
Full source
instance op_epi_of_mono {A B : C} (f : A ⟶ B) [Mono f] : Epi f.op :=
⟨fun _ _ eq => Quiver.Hom.unop_inj ((cancel_mono f).1 (Quiver.Hom.op_inj eq))⟩Informal description
For any monomorphism $f : A \to B$ in a category $C$, the opposite morphism $f^{\mathrm{op}} : B^{\mathrm{op}} \to A^{\mathrm{op}}$ in the opposite category $C^{\mathrm{op}}$ is an epimorphism.
CategoryTheory.SplitMono
structure
{X Y : C} (f : X ⟶ Y)
Full source
/-- A split monomorphism is a morphism `f : X ⟶ Y` with a given retraction `retraction f : Y ⟶ X`
such that `f ≫ retraction f = 𝟙 X`.
Every split monomorphism is a monomorphism.
-/
@[ext, aesop apply safe (rule_sets := [CategoryTheory])]
structure SplitMono {X Y : C} (f : X ⟶ Y) where
/-- The map splitting `f` -/
retraction : Y ⟶ X
/-- `f` composed with `retraction` is the identity -/
id : f ≫ retraction = 𝟙 X := by aesop_catInformal description
A split monomorphism is a morphism \( f: X \to Y \) in a category \( C \) for which there exists a retraction \( \text{retraction } f: Y \to X \) such that the composition \( f \circ (\text{retraction } f) \) equals the identity morphism \( \text{id}_X \).
CategoryTheory.IsSplitMono
structure
{X Y : C} (f : X ⟶ Y)
Full source
/-- `IsSplitMono f` is the assertion that `f` admits a retraction -/
class IsSplitMono {X Y : C} (f : X ⟶ Y) : Prop where
/-- There is a splitting -/
exists_splitMono : Nonempty (SplitMono f)Informal description
The structure `IsSplitMono f` asserts that a morphism $f: X \to Y$ in a category $\mathcal{C}$ has a retraction, i.e., there exists a morphism $g: Y \to X$ such that $g \circ f = \text{id}_X$.
CategoryTheory.SplitMono.comp
definition
{X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (smf : SplitMono f) (smg : SplitMono g) : SplitMono (f ≫ g)
Full source
/-- A composition of `SplitMono` is a `SplitMono`. -/
@[simps]
def SplitMono.comp {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (smf : SplitMono f) (smg : SplitMono g) :
SplitMono (f ≫ g) where
retraction := smg.retraction ≫ smf.retraction
Informal description
Given morphisms \( f: X \to Y \) and \( g: Y \to Z \) in a category \( C \), if both \( f \) and \( g \) are split monomorphisms, then their composition \( f \circ g \) is also a split monomorphism. The retraction of the composition is given by the composition of the retractions of \( g \) and \( f \) in reverse order.
CategoryTheory.IsSplitMono.mk'
theorem
{X Y : C} {f : X ⟶ Y} (sm : SplitMono f) : IsSplitMono f
Full source
/-- A constructor for `IsSplitMono f` taking a `SplitMono f` as an argument -/
theorem IsSplitMono.mk' {X Y : C} {f : X ⟶ Y} (sm : SplitMono f) : IsSplitMono f :=
⟨Nonempty.intro sm⟩Informal description
Given a morphism $f: X \to Y$ in a category $\mathcal{C}$, if $f$ is a split monomorphism (i.e., there exists a retraction $g: Y \to X$ such that $g \circ f = \text{id}_X$), then $f$ satisfies the property of being a split monomorphism.
CategoryTheory.SplitEpi
structure
{X Y : C} (f : X ⟶ Y)
Full source
/-- A split epimorphism is a morphism `f : X ⟶ Y` with a given section `section_ f : Y ⟶ X`
such that `section_ f ≫ f = 𝟙 Y`.
(Note that `section` is a reserved keyword, so we append an underscore.)
Every split epimorphism is an epimorphism.
-/
@[ext, aesop apply safe (rule_sets := [CategoryTheory])]
structure SplitEpi {X Y : C} (f : X ⟶ Y) where
/-- The map splitting `f` -/
section_ : Y ⟶ X
/-- `section_` composed with `f` is the identity -/
id : section_ ≫ f = 𝟙 Y := by aesop_catInformal description
A split epimorphism is a morphism \( f : X \to Y \) in a category \( C \) for which there exists a section \( s : Y \to X \) such that the composition \( s \circ f \) is the identity morphism on \( Y \). Every split epimorphism is an epimorphism.
CategoryTheory.IsSplitEpi
structure
{X Y : C} (f : X ⟶ Y)
Full source
/-- `IsSplitEpi f` is the assertion that `f` admits a section -/
class IsSplitEpi {X Y : C} (f : X ⟶ Y) : Prop where
/-- There is a splitting -/
exists_splitEpi : Nonempty (SplitEpi f)Informal description
The structure `IsSplitEpi f` asserts that the morphism \( f : X \to Y \) in a category \( C \) admits a section, i.e., there exists a morphism \( g : Y \to X \) such that \( f \circ g = \text{id}_Y \).
CategoryTheory.SplitEpi.comp
definition
{X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (sef : SplitEpi f) (seg : SplitEpi g) : SplitEpi (f ≫ g)
Full source
/-- A composition of `SplitEpi` is a split `SplitEpi`. -/
@[simps]
def SplitEpi.comp {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (sef : SplitEpi f) (seg : SplitEpi g) :
SplitEpi (f ≫ g) where
section_ := seg.section_ ≫ sef.section_
Informal description
Given split epimorphisms \( f : X \to Y \) and \( g : Y \to Z \) in a category \( C \), their composition \( f \circ g : X \to Z \) is also a split epimorphism, with the section given by the composition of the sections of \( g \) and \( f \).
CategoryTheory.IsSplitEpi.mk'
theorem
{X Y : C} {f : X ⟶ Y} (se : SplitEpi f) : IsSplitEpi f
Full source
/-- A constructor for `IsSplitEpi f` taking a `SplitEpi f` as an argument -/
theorem IsSplitEpi.mk' {X Y : C} {f : X ⟶ Y} (se : SplitEpi f) : IsSplitEpi f :=
⟨Nonempty.intro se⟩Informal description
Given a split epimorphism \( f : X \to Y \) in a category \( C \), the morphism \( f \) is a split epimorphism (i.e., there exists a section \( s : Y \to X \) such that \( f \circ s = \text{id}_Y \)).
CategoryTheory.retraction
definition
{X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] : Y ⟶ X
Full source
/-- The chosen retraction of a split monomorphism. -/
noncomputable def retraction {X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] : Y ⟶ X :=
hf.exists_splitMono.some.retractionInformal description
Given a split monomorphism \( f : X \to Y \) in a category \( \mathcal{C} \), the retraction of \( f \) is a morphism \( Y \to X \) such that its composition with \( f \) yields the identity morphism on \( X \).
CategoryTheory.IsSplitMono.id
theorem
{X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] : f ≫ retraction f = 𝟙 X
Full source
@[reassoc (attr := simp)]
theorem IsSplitMono.id {X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] : f ≫ retraction f = 𝟙 X :=
hf.exists_splitMono.some.idInformal description
For any split monomorphism $f: X \to Y$ in a category $\mathcal{C}$, the composition of $f$ with its retraction equals the identity morphism on $X$, i.e., $f \circ \text{retraction}(f) = \text{id}_X$.
CategoryTheory.SplitMono.splitEpi
definition
{X Y : C} {f : X ⟶ Y} (sm : SplitMono f) : SplitEpi sm.retraction
Full source
/-- The retraction of a split monomorphism has an obvious section. -/
def SplitMono.splitEpi {X Y : C} {f : X ⟶ Y} (sm : SplitMono f) : SplitEpi sm.retraction where
section_ := f
Informal description
Given a split monomorphism \( f : X \to Y \) in a category \( C \), the retraction of \( f \) is a split epimorphism. That is, there exists a section \( s : Y \to X \) such that the composition \( s \circ f \) is the identity morphism on \( Y \).
CategoryTheory.retraction_isSplitEpi
instance
{X Y : C} (f : X ⟶ Y) [IsSplitMono f] : IsSplitEpi (retraction f)
Full source
/-- The retraction of a split monomorphism is itself a split epimorphism. -/
instance retraction_isSplitEpi {X Y : C} (f : X ⟶ Y) [IsSplitMono f] :
IsSplitEpi (retraction f) :=
IsSplitEpi.mk' (SplitMono.splitEpi _)Informal description
For any split monomorphism $f : X \to Y$ in a category $\mathcal{C}$, the retraction of $f$ is a split epimorphism.
CategoryTheory.isIso_of_epi_of_isSplitMono
theorem
{X Y : C} (f : X ⟶ Y) [IsSplitMono f] [Epi f] : IsIso f
Full source
/-- A split mono which is epi is an iso. -/
theorem isIso_of_epi_of_isSplitMono {X Y : C} (f : X ⟶ Y) [IsSplitMono f] [Epi f] : IsIso f :=
⟨⟨retraction f, ⟨by simp, by simp [← cancel_epi f]⟩⟩⟩Informal description
In any category $\mathcal{C}$, a morphism $f \colon X \to Y$ that is both a split monomorphism and an epimorphism is an isomorphism.
CategoryTheory.section_
definition
{X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] : Y ⟶ X
Full source
/-- The chosen section of a split epimorphism.
(Note that `section` is a reserved keyword, so we append an underscore.)
-/
noncomputable def section_ {X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] : Y ⟶ X :=
hf.exists_splitEpi.some.section_Informal description
Given a split epimorphism \( f : X \to Y \) in a category \( C \), the function returns a section \( s : Y \to X \) of \( f \), i.e., a morphism satisfying \( f \circ s = \text{id}_Y \).
CategoryTheory.IsSplitEpi.id
theorem
{X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] : section_ f ≫ f = 𝟙 Y
Full source
@[reassoc (attr := simp)]
theorem IsSplitEpi.id {X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] : section_section_ f ≫ f = 𝟙 Y :=
hf.exists_splitEpi.some.idInformal description
For any split epimorphism $f \colon X \to Y$ in a category $\mathcal{C}$, the composition of its section $s \colon Y \to X$ with $f$ is the identity morphism on $Y$, i.e., $s \circ f = \mathrm{id}_Y$.
CategoryTheory.SplitEpi.splitMono
definition
{X Y : C} {f : X ⟶ Y} (se : SplitEpi f) : SplitMono se.section_
Full source
/-- The section of a split epimorphism has an obvious retraction. -/
def SplitEpi.splitMono {X Y : C} {f : X ⟶ Y} (se : SplitEpi f) : SplitMono se.section_ where
retraction := f
Informal description
Given a split epimorphism \( f : X \to Y \) in a category \( C \), the section \( s : Y \to X \) of \( f \) is a split monomorphism, with \( f \) itself serving as its retraction.
CategoryTheory.section_isSplitMono
instance
{X Y : C} (f : X ⟶ Y) [IsSplitEpi f] : IsSplitMono (section_ f)
Full source
/-- The section of a split epimorphism is itself a split monomorphism. -/
instance section_isSplitMono {X Y : C} (f : X ⟶ Y) [IsSplitEpi f] : IsSplitMono (section_ f) :=
IsSplitMono.mk' (SplitEpi.splitMono _)Informal description
For any split epimorphism $f : X \to Y$ in a category $\mathcal{C}$, the section $s : Y \to X$ of $f$ is a split monomorphism.
CategoryTheory.isIso_of_mono_of_isSplitEpi
theorem
{X Y : C} (f : X ⟶ Y) [Mono f] [IsSplitEpi f] : IsIso f
Full source
/-- A split epi which is mono is an iso. -/
theorem isIso_of_mono_of_isSplitEpi {X Y : C} (f : X ⟶ Y) [Mono f] [IsSplitEpi f] : IsIso f :=
⟨⟨section_ f, ⟨by simp [← cancel_mono f], by simp⟩⟩⟩Informal description
Let $f \colon X \to Y$ be a morphism in a category $\mathcal{C}$. If $f$ is both a monomorphism and a split epimorphism, then $f$ is an isomorphism.
CategoryTheory.IsSplitMono.of_iso
instance
{X Y : C} (f : X ⟶ Y) [IsIso f] : IsSplitMono f
Full source
/-- Every iso is a split mono. -/
instance (priority := 100) IsSplitMono.of_iso {X Y : C} (f : X ⟶ Y) [IsIso f] : IsSplitMono f :=
IsSplitMono.mk' { retraction := inv f }Informal description
For any isomorphism $f : X \to Y$ in a category $\mathcal{C}$, $f$ is a split monomorphism. That is, there exists a morphism $g : Y \to X$ such that $g \circ f = \text{id}_X$.
CategoryTheory.IsSplitEpi.of_iso
instance
{X Y : C} (f : X ⟶ Y) [IsIso f] : IsSplitEpi f
Full source
/-- Every iso is a split epi. -/
instance (priority := 100) IsSplitEpi.of_iso {X Y : C} (f : X ⟶ Y) [IsIso f] : IsSplitEpi f :=
IsSplitEpi.mk' { section_ := inv f }Informal description
For any isomorphism $f : X \to Y$ in a category $\mathcal{C}$, $f$ is a split epimorphism. That is, there exists a morphism $g : Y \to X$ such that $f \circ g = \text{id}_Y$.
CategoryTheory.SplitMono.mono
theorem
{X Y : C} {f : X ⟶ Y} (sm : SplitMono f) : Mono f
Full source
theorem SplitMono.mono {X Y : C} {f : X ⟶ Y} (sm : SplitMono f) : Mono f :=
{ right_cancellation := fun g h w => by replace w := w =≫ sm.retraction; simpa using w }Informal description
For any morphism \( f: X \to Y \) in a category \( C \), if \( f \) is a split monomorphism, then \( f \) is a monomorphism.
CategoryTheory.IsSplitMono.mono
instance
{X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] : Mono f
Full source
/-- Every split mono is a mono. -/
instance (priority := 100) IsSplitMono.mono {X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] : Mono f :=
hf.exists_splitMono.some.monoInformal description
For any morphism $f \colon X \to Y$ in a category $\mathcal{C}$, if $f$ is a split monomorphism, then $f$ is a monomorphism.
CategoryTheory.SplitEpi.epi
theorem
{X Y : C} {f : X ⟶ Y} (se : SplitEpi f) : Epi f
Full source
theorem SplitEpi.epi {X Y : C} {f : X ⟶ Y} (se : SplitEpi f) : Epi f :=
{ left_cancellation := fun g h w => by replace w := se.section_ ≫= w; simpa using w }Informal description
For any morphism $f \colon X \to Y$ in a category $\mathcal{C}$, if $f$ is a split epimorphism, then $f$ is an epimorphism.
CategoryTheory.IsSplitEpi.epi
instance
{X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] : Epi f
Full source
/-- Every split epi is an epi. -/
instance (priority := 100) IsSplitEpi.epi {X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] : Epi f :=
hf.exists_splitEpi.some.epiInformal description
For any morphism $f \colon X \to Y$ in a category $\mathcal{C}$, if $f$ is a split epimorphism, then $f$ is an epimorphism.
CategoryTheory.instIsSplitMonoComp
instance
{X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [hf : IsSplitMono f] [hg : IsSplitMono g] : IsSplitMono (f ≫ g)
Full source
instance {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [hf : IsSplitMono f] [hg : IsSplitMono g] :
IsSplitMono (f ≫ g) := IsSplitMono.mk' <| hf.exists_splitMono.some.comp hg.exists_splitMono.someInformal description
For any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, if both $f$ and $g$ are split monomorphisms, then their composition $f \circ g$ is also a split monomorphism.
CategoryTheory.instIsSplitEpiComp
instance
{X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [hf : IsSplitEpi f] [hg : IsSplitEpi g] : IsSplitEpi (f ≫ g)
Full source
instance {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [hf : IsSplitEpi f] [hg : IsSplitEpi g] :
IsSplitEpi (f ≫ g) := IsSplitEpi.mk' <| hf.exists_splitEpi.some.comp hg.exists_splitEpi.someInformal description
For any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, if both $f$ and $g$ are split epimorphisms, then their composition $f \circ g$ is also a split epimorphism.
CategoryTheory.IsIso.of_mono_retraction'
theorem
{X Y : C} {f : X ⟶ Y} (hf : SplitMono f) [Mono <| hf.retraction] : IsIso f
Full source
/-- Every split mono whose retraction is mono is an iso. -/
theorem IsIso.of_mono_retraction' {X Y : C} {f : X ⟶ Y} (hf : SplitMono f) [Mono <| hf.retraction] :
IsIso f :=
⟨⟨hf.retraction, ⟨by simp, (cancel_mono_id <| hf.retraction).mp (by simp)⟩⟩⟩Informal description
Let \( f : X \to Y \) be a split monomorphism in a category \( \mathcal{C} \). If the retraction \( r : Y \to X \) of \( f \) is a monomorphism, then \( f \) is an isomorphism.
CategoryTheory.IsIso.of_mono_retraction
theorem
{X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] [hf' : Mono <| retraction f] : IsIso f
Full source
/-- Every split mono whose retraction is mono is an iso. -/
theorem IsIso.of_mono_retraction {X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f]
[hf' : Mono <| retraction f] : IsIso f :=
@IsIso.of_mono_retraction' _ _ _ _ _ hf.exists_splitMono.some hf'Informal description
Let \( f : X \to Y \) be a split monomorphism in a category \( \mathcal{C} \). If the retraction \( r : Y \to X \) of \( f \) is a monomorphism, then \( f \) is an isomorphism.
CategoryTheory.IsIso.of_epi_section'
theorem
{X Y : C} {f : X ⟶ Y} (hf : SplitEpi f) [Epi <| hf.section_] : IsIso f
Full source
/-- Every split epi whose section is epi is an iso. -/
theorem IsIso.of_epi_section' {X Y : C} {f : X ⟶ Y} (hf : SplitEpi f) [Epi <| hf.section_] :
IsIso f :=
⟨⟨hf.section_, ⟨(cancel_epi_id <| hf.section_).mp (by simp), by simp⟩⟩⟩Informal description
Let \( f : X \to Y \) be a split epimorphism in a category \( C \). If the section \( s : Y \to X \) of \( f \) is an epimorphism, then \( f \) is an isomorphism.
CategoryTheory.IsIso.of_epi_section
theorem
{X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] [hf' : Epi <| section_ f] : IsIso f
Full source
/-- Every split epi whose section is epi is an iso. -/
theorem IsIso.of_epi_section {X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] [hf' : Epi <| section_ f] :
IsIso f :=
@IsIso.of_epi_section' _ _ _ _ _ hf.exists_splitEpi.some hf'Informal description
Let \( f : X \to Y \) be a split epimorphism in a category \( \mathcal{C} \). If the section \( s : Y \to X \) of \( f \) is an epimorphism, then \( f \) is an isomorphism.
CategoryTheory.Groupoid.ofTruncSplitMono
definition
(all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)) : Groupoid.{v₁} C
Full source
/-- A category where every morphism has a `Trunc` retraction is computably a groupoid. -/
noncomputable def Groupoid.ofTruncSplitMono
(all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)) : Groupoid.{v₁} C := by
apply Groupoid.ofIsIso
intro X Y f
have ⟨a,_⟩ := Trunc.exists_rep <| all_split_mono f
have ⟨b,_⟩ := Trunc.exists_rep <| all_split_mono <| retraction f
apply IsIso.of_mono_retractionInformal description
Given a category \( C \) where every morphism \( f : X \to Y \) has a truncated retraction (i.e., there exists a morphism \( g : Y \to X \) such that \( g \circ f = \text{id}_X \), and this existence is truncated), then \( C \) is a groupoid. In other words, every morphism in \( C \) is an isomorphism.
CategoryTheory.SplitMonoCategory
structure
Full source
/-- A split mono category is a category in which every monomorphism is split. -/
class SplitMonoCategory : Prop where
/-- All monos are split -/
isSplitMono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [Mono f], IsSplitMono fInformal description
A split mono category is a category in which every monomorphism has a left inverse (i.e., every monomorphism is split). This means for every monomorphism $f: X \rightarrow Y$, there exists a morphism $g: Y \rightarrow X$ such that $g \circ f = \text{id}_X$.
CategoryTheory.SplitEpiCategory
structure
Full source
/-- A split epi category is a category in which every epimorphism is split. -/
class SplitEpiCategory : Prop where
/-- All epis are split -/
isSplitEpi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [Epi f], IsSplitEpi fInformal description
A split epi category is a category in which every epimorphism admits a section, meaning for every epimorphism $f: X \to Y$, there exists a morphism $g: Y \to X$ such that $f \circ g = \text{id}_Y$.
CategoryTheory.isSplitMono_of_mono
theorem
[SplitMonoCategory C] {X Y : C} (f : X ⟶ Y) [Mono f] : IsSplitMono f
Full source
/-- In a category in which every monomorphism is split, every monomorphism splits. This is not an
instance because it would create an instance loop. -/
theorem isSplitMono_of_mono [SplitMonoCategory C] {X Y : C} (f : X ⟶ Y) [Mono f] : IsSplitMono f :=
SplitMonoCategory.isSplitMono_of_mono _Informal description
In a split mono category $\mathcal{C}$, every monomorphism $f: X \to Y$ is split, i.e., there exists a morphism $g: Y \to X$ such that $g \circ f = \text{id}_X$.
CategoryTheory.isSplitEpi_of_epi
theorem
[SplitEpiCategory C] {X Y : C} (f : X ⟶ Y) [Epi f] : IsSplitEpi f
Full source
/-- In a category in which every epimorphism is split, every epimorphism splits. This is not an
instance because it would create an instance loop. -/
theorem isSplitEpi_of_epi [SplitEpiCategory C] {X Y : C} (f : X ⟶ Y) [Epi f] : IsSplitEpi f :=
SplitEpiCategory.isSplitEpi_of_epi _Informal description
In a split epi category $\mathcal{C}$, every epimorphism $f: X \to Y$ is split, i.e., there exists a morphism $g: Y \to X$ such that $f \circ g = \text{id}_Y$.
CategoryTheory.SplitMono.map
definition
{X Y : C} {f : X ⟶ Y} (sm : SplitMono f) (F : C ⥤ D) : SplitMono (F.map f)
Full source
/-- Split monomorphisms are also absolute monomorphisms. -/
@[simps]
def SplitMono.map {X Y : C} {f : X ⟶ Y} (sm : SplitMono f) (F : C ⥤ D) : SplitMono (F.map f) where
retraction := F.map sm.retraction
id := by rw [← Functor.map_comp, SplitMono.id, Functor.map_id]Informal description
Given a split monomorphism \( f: X \to Y \) in a category \( C \) and a functor \( F: C \to D \), the morphism \( F(f): F(X) \to F(Y) \) in \( D \) is also a split monomorphism, with retraction given by \( F \) applied to the retraction of \( f \).
CategoryTheory.SplitEpi.map
definition
{X Y : C} {f : X ⟶ Y} (se : SplitEpi f) (F : C ⥤ D) : SplitEpi (F.map f)
Full source
/-- Split epimorphisms are also absolute epimorphisms. -/
@[simps]
def SplitEpi.map {X Y : C} {f : X ⟶ Y} (se : SplitEpi f) (F : C ⥤ D) : SplitEpi (F.map f) where
section_ := F.map se.section_
id := by rw [← Functor.map_comp, SplitEpi.id, Functor.map_id]Informal description
Given a split epimorphism \( f : X \to Y \) in a category \( C \) and a functor \( F : C \to D \), the morphism \( F(f) : F(X) \to F(Y) \) in \( D \) is also a split epimorphism, with section given by \( F \) applied to the section of \( f \).
CategoryTheory.instIsSplitMonoMap
instance
{X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] (F : C ⥤ D) : IsSplitMono (F.map f)
Full source
instance {X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] (F : C ⥤ D) : IsSplitMono (F.map f) :=
IsSplitMono.mk' (hf.exists_splitMono.some.map F)Informal description
For any split monomorphism $f: X \to Y$ in a category $\mathcal{C}$ and any functor $F: \mathcal{C} \to \mathcal{D}$, the morphism $F(f): F(X) \to F(Y)$ in $\mathcal{D}$ is also a split monomorphism.
CategoryTheory.instIsSplitEpiMap
instance
{X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] (F : C ⥤ D) : IsSplitEpi (F.map f)
Full source
instance {X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] (F : C ⥤ D) : IsSplitEpi (F.map f) :=
IsSplitEpi.mk' (hf.exists_splitEpi.some.map F)Informal description
For any split epimorphism $f: X \to Y$ in a category $\mathcal{C}$ and any functor $F: \mathcal{C} \to \mathcal{D}$, the morphism $F(f): F(X) \to F(Y)$ in $\mathcal{D}$ is also a split epimorphism.