Induction principles for structured and costructured arrows

Assume that L : C ⥤ D is a localization functor for W : MorphismProperty C. Given X : C and a predicate P on StructuredArrow (L.obj X) L, we obtain the lemma Localization.induction_structuredArrow which shows that P holds for all structured arrows if P holds for the identity map 𝟙 (L.obj X), if P is stable by post-composition with L.map f for any f and if P is stable by post-composition with the inverse of L.map w when W w.

We obtain a similar lemma Localization.induction_costructuredArrow for costructured arrows.

@[simp]

theorem CategoryTheory.Localization.structuredArrowEquiv_symm_apply {C : Type u_1} {D : Type u_2} {D' : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} D'] (W : CategoryTheory.MorphismProperty C) (L : CategoryTheory.Functor C D) (L' : CategoryTheory.Functor C D') [L.IsLocalization W] [L'.IsLocalization W] {X : C} (f : CategoryTheory.StructuredArrow (L'.obj X) L') : (CategoryTheory.Localization.structuredArrowEquiv W L L').symm f = CategoryTheory.StructuredArrow.mk ((CategoryTheory.Localization.homEquiv W L' L) f.hom)

@[simp]

theorem CategoryTheory.Localization.structuredArrowEquiv_apply {C : Type u_1} {D : Type u_2} {D' : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} D'] (W : CategoryTheory.MorphismProperty C) (L : CategoryTheory.Functor C D) (L' : CategoryTheory.Functor C D') [L.IsLocalization W] [L'.IsLocalization W] {X : C} (f : CategoryTheory.StructuredArrow (L.obj X) L) : (CategoryTheory.Localization.structuredArrowEquiv W L L') f = CategoryTheory.StructuredArrow.mk ((CategoryTheory.Localization.homEquiv W L L') f.hom)

noncomputable def CategoryTheory.Localization.structuredArrowEquiv {C : Type u_1} {D : Type u_2} {D' : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} D'] (W : CategoryTheory.MorphismProperty C) (L : CategoryTheory.Functor C D) (L' : CategoryTheory.Functor C D') [L.IsLocalization W] [L'.IsLocalization W] {X : C} : CategoryTheory.StructuredArrow (L.obj X) L ≃ CategoryTheory.StructuredArrow (L'.obj X) L'

The bijection StructuredArrow (L.obj X) L ≃ StructuredArrow (L'.obj X) L' when L and L' are two localization functors for the same class of morphisms.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Localization.induction_structuredArrow {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] {X : C} (P : CategoryTheory.StructuredArrow (L.obj X) L → Prop) (hP₀ : P (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.id (L.obj X)))) (hP₁ : ∀ ⦃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)))) (hP₂ : ∀ ⦃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

theorem CategoryTheory.Localization.induction_costructuredArrow {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] {Y : C} (P : CategoryTheory.CostructuredArrow L (L.obj Y) → Prop) (hP₀ : P (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.id (L.obj Y)))) (hP₁ : ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂) (φ : L.obj X₂ ⟶ L.obj Y), P (CategoryTheory.CostructuredArrow.mk φ) → P (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (L.map f) φ))) (hP₂ : ∀ ⦃X₁ X₂ : C⦄ (w : X₁ ⟶ X₂) (hw : W w) (φ : L.obj X₁ ⟶ L.obj Y), P (CategoryTheory.CostructuredArrow.mk φ) → P (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.isoOfHom L W w hw).inv φ))) (g : CategoryTheory.CostructuredArrow L (L.obj Y)) : P g