Theorems · Theorem · category theory

CategoryTheory.Localization.induction_structuredArrow

∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W] {X : C}
  (P : CategoryTheory.StructuredArrow (L.obj X) L → Prop),
  P (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.id (L.obj X))) →
    (∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁),
        P (CategoryTheory.StructuredArrow.mk φ) →
          P (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp φ (L.map f)))) →
      (∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
          P (CategoryTheory.StructuredArrow.mk φ) →
            P
              (CategoryTheory.StructuredArrow.mk
                (CategoryTheory.CategoryStruct.comp φ (CategoryTheory.Localization.isoOfHom L W w hw).inv))) →
        ∀ (g : CategoryTheory.StructuredArrow (L.obj X) L), P g

Defined in

Mathlib.CategoryTheory.Localization.StructuredArrow

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocalization