Theorems · Theorem · category theory

CategoryTheory.TwoSquare.GuitartExact.quotient_of_nonempty_leftHomotopy

∀ {C₀ : Type u_1} {C : Type u_2} {H₀ : Type u_3} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₀]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Category.{v_3, u_3} H₀]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} H] {T : CategoryTheory.Functor C₀ H₀} {L : CategoryTheory.Functor C₀ C}
  {R : CategoryTheory.Functor H₀ H} {B : CategoryTheory.Functor C H} [T.EssSurj] [T.Full] [B.Full]
  (e : T.comp R ≅ L.comp B),
  (∀ ⦃X₀ : C₀⦄ ⦃Y : C⦄ (f₀ f₁ : L.obj X₀ ⟶ Y),
      B.map f₀ = B.map f₁ → ∃ P, T.map P.i₀ = T.map P.i₁ ∧ Nonempty ((P.map L).LeftHomotopy f₀ f₁)) →
    CategoryTheory.TwoSquare.GuitartExact e.hom

Defined in

Mathlib.CategoryTheory.GuitartExact.Quotient

Cited by

1 results in Mathlib

Foundations

Depth 44 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.EssSurjCategoryTheory.Functor.FullCategoryTheory.Functor.Full