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.

source
noncomputable def CategoryTheory.Localization.structuredArrowEquiv {C : Type u_1} {D : Type u_2} {D' : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, 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.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Localization.structuredArrowEquiv_apply {C : Type u_1} {D : Type u_2} {D' : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, 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)
    source
    @[simp]
    theorem CategoryTheory.Localization.structuredArrowEquiv_symm_apply {C : Type u_1} {D : Type u_2} {D' : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, 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)
    source
    theorem CategoryTheory.Localization.induction_structuredArrow {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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
    source
    theorem CategoryTheory.Localization.induction_costructuredArrow {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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