Theorems · Theorem · category theory

CategoryTheory.TwoSquare.GuitartExact.quotient_of_nonempty_rightHomotopy

∀ {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₁ : X ⟶ L.obj Y₀),
      B.map f₀ = B.map f₁ → ∃ P, T.map P.p₀ = T.map P.p₁ ∧ Nonempty ((P.map L).RightHomotopy f₀ f₁)) →
    CategoryTheory.TwoSquare.GuitartExact e.inv

Defined in

Mathlib.CategoryTheory.GuitartExact.Quotient

Cited by

0 results in Mathlib

Foundations

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

Assumes

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