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_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)
@[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)
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.
Instances For
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