CategoryTheory.Precoherent.pullback
theorem CategoryTheory.Precoherent.pullback :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [self : CategoryTheory.Precoherent C] {B₁ B₂ : C}
(f : B₂ ⟶ B₁) (α : Type) [inst_1 : Finite α] (X₁ : α → C) (π₁ : (a : α) → X₁ a ⟶ B₁),
CategoryTheory.EffectiveEpiFamily X₁ π₁ →
∃ β,
∃ (_ : Finite β),
∃ X₂ π₂,
CategoryTheory.EffectiveEpiFamily X₂ π₂ ∧
∃ i ι,
∀ (b : β),
CategoryTheory.CategoryStruct.comp (ι b) (π₁ (i b)) = CategoryTheory.CategoryStruct.comp (π₂ b) f
The theorem `CategoryTheory.Precoherent.pullback` states that for any category `C` that is precoherent, and given two objects `B₁` and `B₂` in `C`, along with a morphism `f` from `B₂` to `B₁`, if there exists an effective epi family `π₁` over `B₁`, then there also exists an effective epi family `π₂` over `B₂`. Furthermore, `π₂` factors through `π₁`, meaning that for each element `b` of `β`, the composition of morphisms `(ι b) ≫ (π₁ (i b))` is equivalent to `(π₂ b) ≫ f`. This theorem is essentially asserting the existence of a pullback in the category `C` for the given morphism `f` and effective epi family `π₁`.
More concisely: Given a precoherent category `C`, a morphism `f: B₂ -> B₁` from objects `B₁` and `B₂`, and an effective epimorphism `π₁: π₁ → B₁` over `B₁`, there exists an effective epimorphism `π₂: π₂ → B₂` over `B₂` such that `π₂ ∘ f ≈ π₁`.
|
CategoryTheory.Preregular.exists_fac
theorem CategoryTheory.Preregular.exists_fac :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [self : CategoryTheory.Preregular C] {X Y Z : C}
(f : X ⟶ Y) (g : Z ⟶ Y) [inst_1 : CategoryTheory.EffectiveEpi g],
∃ W h,
∃ (_ : CategoryTheory.EffectiveEpi h),
∃ i, CategoryTheory.CategoryStruct.comp i g = CategoryTheory.CategoryStruct.comp h f
The theorem `CategoryTheory.Preregular.exists_fac` in the Category Theory asserts that given a category `C` and three objects `X`, `Y`, `Z` in `C`, and two morphisms `f : X ⟶ Y` and `g : Z ⟶ Y` where `g` is an effective epimorphism, there exists an object `W`, an effective epimorphism `h : W ⟶ X`, and a morphism `i : W ⟶ Z` such that the diagram commutes. That is, the composition of `i` and `g` equals the composition of `h` and `f`. This theorem describes the existence of certain commutative diagrams in categories, which is a fundamental concept in category theory.
More concisely: Given a category `C`, objects `X`, `Y`, `Z`, morphisms `f : X ⟶ Y`, `g : Z ⟶ Y` with `g` an effective epimorphism, there exists an object `W`, effective epimorphism `h : W ⟶ X`, and morphism `i : W ⟶ Z` such that `h × g = i × f`. (This statement asserts the existence of a commutative square with given morphisms as legs.)
|