@[reducible, inline]

abbrev AlgebraicTopologyI.SimplicialObject (C : Type u) [CategoryTheory.Category.{v, u} C] : Type (max v u)

Definition 4.2 (Simplicial object). A simplicial object in a category C is a functor Δ^{op} → C from the opposite of the simplex category. This is a thin wrapper around Mathlib's CategoryTheory.SimplicialObject.

@[reducible, inline]

abbrev AlgebraicTopologyI.SimplexCategoryInj : Type

Definition 4.3 (Injective simplex category). The wide subcategory of SimplexCategory whose morphisms are the injective (monomorphism) simplex maps. Equivalent to the subcategory of strictly order-preserving maps [m] → [n].

@[reducible, inline]

abbrev AlgebraicTopologyI.IsSplitEpi {C : Type u} [CategoryTheory.Category.{v, u} C] {A B : C} (f : A ⟶ B) : Prop

Definition 4.5 (Split epimorphism). A morphism f : A ⟶ B is a split epimorphism if it admits a right inverse, i.e. there exists s : B ⟶ A with s ≫ f = 𝟙 B. Thin wrapper around CategoryTheory.IsSplitEpi.

@[reducible, inline]

abbrev AlgebraicTopologyI.SplitMonomorphism {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : Type v

Definition 4.5 (Split monomorphism). A morphism f : X ⟶ Y is a split monomorphism if it admits a left inverse, i.e. there exists r : Y ⟶ X with f ≫ r = 𝟙 X. Thin wrapper around CategoryTheory.SplitMono.

theorem AlgebraicTopologyI.functor_map_isSplitEpi {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y) [IsSplitEpi f] : IsSplitEpi (F.map f)

Lemma 4.7 (Split epis are preserved by functors), first half. If f : X ⟶ Y is a split epimorphism in C, then F.map f is a split epimorphism in D for any functor F : C ⥤ D. Functors preserve any diagram involving only composition and identities, so they automatically preserve splittings.

theorem AlgebraicTopologyI.functor_map_isSplitMono {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsSplitMono f] : CategoryTheory.IsSplitMono (F.map f)

Lemma 4.7 (Split monos are preserved by functors), second half. If f : X ⟶ Y is a split monomorphism in C, then F.map f is a split monomorphism in D for any functor F : C ⥤ D.

theorem AlgebraicTopologyI.functor_preserves_split {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y) : (IsSplitEpi f → IsSplitEpi (F.map f)) ∧ (CategoryTheory.IsSplitMono f → CategoryTheory.IsSplitMono (F.map f))

Lemma 4.7 (Functors preserve splittings). Packaged form of the two preceding theorems: any functor F : C ⥤ D sends split epimorphisms to split epimorphisms and split monomorphisms to split monomorphisms.

theorem AlgebraicTopologyI.isIso_iff_isSplitEpi_and_isSplitMono {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ IsSplitEpi f ∧ CategoryTheory.IsSplitMono f

Lemma 4.8. A morphism f : X ⟶ Y in a category is an isomorphism if and only if it is both a split epimorphism and a split monomorphism. The forward direction is immediate (an inverse is a one-sided inverse on each side). The reverse direction uses that a monic split epimorphism is automatically iso.