Morphism properties that are inverted by a functor #
In this file, we introduce the predicate P.IsInvertedBy F which expresses
that the morphisms satisfying P : MorphismProperty C are mapped to
isomorphisms by a functor F : C ⥤ D.
This is used in the localization of categories API (folder CategoryTheory.Localization).
def
CategoryTheory.MorphismProperty.IsInvertedBy
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(P : MorphismProperty C)
(F : Functor C D)
:
If P : MorphismProperty C and F : C ⥤ D, then
P.IsInvertedBy F means that all morphisms in P are mapped by F
to isomorphisms in D.
Equations
- P.IsInvertedBy F = ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P f → CategoryTheory.IsIso (F.map f)
Instances For
theorem
CategoryTheory.MorphismProperty.IsInvertedBy.of_le
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(P Q : MorphismProperty C)
(F : Functor C D)
(hQ : Q.IsInvertedBy F)
(h : P ≤ Q)
:
P.IsInvertedBy F
theorem
CategoryTheory.MorphismProperty.IsInvertedBy.of_comp
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_4, u_1} C₁]
[Category.{u_5, u_2} C₂]
[Category.{u_6, u_3} C₃]
(W : MorphismProperty C₁)
(F : Functor C₁ C₂)
(hF : W.IsInvertedBy F)
(G : Functor C₂ C₃)
:
W.IsInvertedBy (F.comp G)
theorem
CategoryTheory.MorphismProperty.IsInvertedBy.op
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{W : MorphismProperty C}
{L : Functor C D}
(h : W.IsInvertedBy L)
:
W.op.IsInvertedBy L.op
theorem
CategoryTheory.MorphismProperty.IsInvertedBy.rightOp
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{W : MorphismProperty C}
{L : Functor Cᵒᵖ D}
(h : W.op.IsInvertedBy L)
:
W.IsInvertedBy L.rightOp
theorem
CategoryTheory.MorphismProperty.IsInvertedBy.leftOp
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{W : MorphismProperty C}
{L : Functor C Dᵒᵖ}
(h : W.IsInvertedBy L)
:
W.op.IsInvertedBy L.leftOp
theorem
CategoryTheory.MorphismProperty.IsInvertedBy.unop
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{W : MorphismProperty C}
{L : Functor Cᵒᵖ Dᵒᵖ}
(h : W.op.IsInvertedBy L)
:
W.IsInvertedBy L.unop
theorem
CategoryTheory.MorphismProperty.IsInvertedBy.prod
{C₁ : Type u_1}
{C₂ : Type u_2}
[Category.{u_5, u_1} C₁]
[Category.{u_6, u_2} C₂]
{W₁ : MorphismProperty C₁}
{W₂ : MorphismProperty C₂}
{E₁ : Type u_3}
{E₂ : Type u_4}
[Category.{u_7, u_3} E₁]
[Category.{u_8, u_4} E₂]
{F₁ : Functor C₁ E₁}
{F₂ : Functor C₂ E₂}
(h₁ : W₁.IsInvertedBy F₁)
(h₂ : W₂.IsInvertedBy F₂)
:
(W₁.prod W₂).IsInvertedBy (F₁.prod F₂)
theorem
CategoryTheory.MorphismProperty.IsInvertedBy.pi
{J : Type w}
{C : J → Type u}
{D : J → Type u'}
[(j : J) → Category.{v, u} (C j)]
[(j : J) → Category.{v', u'} (D j)]
(W : (j : J) → MorphismProperty (C j))
(F : (j : J) → Functor (C j) (D j))
(hF : ∀ (j : J), (W j).IsInvertedBy (F j))
:
(MorphismProperty.pi W).IsInvertedBy (Functor.pi F)
def
CategoryTheory.MorphismProperty.FunctorsInverting
{C : Type u}
[Category.{v, u} C]
(W : MorphismProperty C)
(D : Type u_1)
[Category.{u_2, u_1} D]
:
Type (max (max (max u u_1) v) u_2)
The full subcategory of C ⥤ D consisting of functors inverting morphisms in W
Equations
- W.FunctorsInverting D = CategoryTheory.FullSubcategory fun (F : CategoryTheory.Functor C D) => W.IsInvertedBy F
Instances For
theorem
CategoryTheory.MorphismProperty.FunctorsInverting.ext
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{W : MorphismProperty C}
{F₁ F₂ : W.FunctorsInverting D}
(h : F₁.obj = F₂.obj)
:
F₁ = F₂
instance
CategoryTheory.MorphismProperty.instCategoryFunctorsInverting
{C : Type u}
[Category.{v, u} C]
(W : MorphismProperty C)
(D : Type u_1)
[Category.{u_2, u_1} D]
:
Category.{max u u_2, max (max (max u_2 u_1) u) v} (W.FunctorsInverting D)
Equations
- W.instCategoryFunctorsInverting D = CategoryTheory.FullSubcategory.category fun (F : CategoryTheory.Functor C D) => W.IsInvertedBy F
theorem
CategoryTheory.MorphismProperty.FunctorsInverting.hom_ext
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{W : MorphismProperty C}
{F₁ F₂ : W.FunctorsInverting D}
{α β : F₁ ⟶ F₂}
(h : α.app = β.app)
:
α = β
def
CategoryTheory.MorphismProperty.FunctorsInverting.mk
{C : Type u}
[Category.{v, u} C]
{W : MorphismProperty C}
{D : Type u_1}
[Category.{u_2, u_1} D]
(F : Functor C D)
(hF : W.IsInvertedBy F)
:
W.FunctorsInverting D
A constructor for W.FunctorsInverting D
Equations
- CategoryTheory.MorphismProperty.FunctorsInverting.mk F hF = { obj := F, property := hF }
Instances For
theorem
CategoryTheory.MorphismProperty.IsInvertedBy.iff_of_iso
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(W : MorphismProperty C)
{F₁ F₂ : Functor C D}
(e : F₁ ≅ F₂)
:
W.IsInvertedBy F₁ ↔ W.IsInvertedBy F₂
@[simp]
theorem
CategoryTheory.MorphismProperty.IsInvertedBy.isoClosure_iff
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(W : MorphismProperty C)
(F : Functor C D)
:
W.isoClosure.IsInvertedBy F ↔ W.IsInvertedBy F
@[simp]
theorem
CategoryTheory.MorphismProperty.IsInvertedBy.iff_comp
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_4, u_1} C₁]
[Category.{u_5, u_2} C₂]
[Category.{u_6, u_3} C₃]
(W : MorphismProperty C₁)
(F : Functor C₁ C₂)
(G : Functor C₂ C₃)
[G.ReflectsIsomorphisms]
:
W.IsInvertedBy (F.comp G) ↔ W.IsInvertedBy F
theorem
CategoryTheory.MorphismProperty.IsInvertedBy.iff_le_inverseImage_isomorphisms
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(W : MorphismProperty C)
(F : Functor C D)
:
W.IsInvertedBy F ↔ W ≤ (isomorphisms D).inverseImage F
theorem
CategoryTheory.MorphismProperty.IsInvertedBy.iff_map_le_isomorphisms
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(W : MorphismProperty C)
(F : Functor C D)
:
W.IsInvertedBy F ↔ W.map F ≤ isomorphisms D
theorem
CategoryTheory.MorphismProperty.IsInvertedBy.map_iff
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_4, u_1} C₁]
[Category.{u_5, u_2} C₂]
[Category.{u_6, u_3} C₃]
(W : MorphismProperty C₁)
(F : Functor C₁ C₂)
(G : Functor C₂ C₃)
:
(W.map F).IsInvertedBy G ↔ W.IsInvertedBy (F.comp G)