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.

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

@[simp]

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

@[simp]

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

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

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