Documentation

Mathlib.CategoryTheory.Localization.StructuredArrow

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} :

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.
Instances For
    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