Construction of the localized category #
This file constructs the localized category, obtained by formally inverting
a class of maps W : MorphismProperty C in a category C.
We first construct a quiver LocQuiver W whose objects are the same as those
of C and whose maps are the maps in C and placeholders for the formal
inverses of the maps in W.
The localized category W.Localization is obtained by taking the quotient
of the path category of LocQuiver W by the congruence generated by four
types of relations.
The obvious functor Q W : C ⥤ W.Localization satisfies the universal property
of the localization. Indeed, if G : C ⥤ D sends morphisms in W to isomorphisms
in D (i.e. we have hG : W.IsInvertedBy G), then there exists a unique functor
G' : W.Localization ⥤ D such that Q W ≫ G' = G. This G' is lift G hG.
The expected property of lift G hG if expressed by the lemma fac and the
uniqueness is expressed by uniq.
References #
- [P. Gabriel, M. Zisman, Calculus of fractions and homotopy theory][gabriel-zisman-1967]
structure
CategoryTheory.Localization.Construction.LocQuiver
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
:
Type uC
- obj : C
underlying object
If W : MorphismProperty C, LocQuiver W is a quiver with the same objects
as C, and whose morphisms are those in C and placeholders for formal
inverses of the morphisms in W.
Instances For
def
CategoryTheory.Localization.Construction.ιPaths
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
(X : C)
:
The object in the path category of LocQuiver W attached to an object in
the category C
Instances For
def
CategoryTheory.Localization.Construction.ψ₁
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
{X : C}
{Y : C}
(f : X ⟶ Y)
:
The morphism in the path category associated to a morphism in the original category.
Instances For
def
CategoryTheory.Localization.Construction.ψ₂
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
{X : C}
{Y : C}
(w : X ⟶ Y)
(hw : W X Y w)
:
The morphism in the path category corresponding to a formal inverse.
Instances For
inductive
CategoryTheory.Localization.Construction.relations
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
:
- id: ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} (X : C), CategoryTheory.Localization.Construction.relations W (CategoryTheory.Localization.Construction.ψ₁ W (CategoryTheory.CategoryStruct.id X)) (CategoryTheory.CategoryStruct.id (CategoryTheory.Localization.Construction.ιPaths W X))
- comp: ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), CategoryTheory.Localization.Construction.relations W (CategoryTheory.Localization.Construction.ψ₁ W (CategoryTheory.CategoryStruct.comp f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Construction.ψ₁ W f) (CategoryTheory.Localization.Construction.ψ₁ W g))
- Winv₁: ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (w : X ⟶ Y) (hw : W w), CategoryTheory.Localization.Construction.relations W (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Construction.ψ₁ W w) (CategoryTheory.Localization.Construction.ψ₂ W w hw)) (CategoryTheory.CategoryStruct.id (CategoryTheory.Localization.Construction.ιPaths W X))
- Winv₂: ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (w : X ⟶ Y) (hw : W w), CategoryTheory.Localization.Construction.relations W (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Construction.ψ₂ W w hw) (CategoryTheory.Localization.Construction.ψ₁ W w)) (CategoryTheory.CategoryStruct.id (CategoryTheory.Localization.Construction.ιPaths W Y))
The relations by which we take the quotient in order to get the localized category.
Instances For
def
CategoryTheory.MorphismProperty.Localization
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
:
Type uC
The localized category obtained by formally inverting the morphisms
in W : MorphismProperty C
Instances For
def
CategoryTheory.MorphismProperty.Q
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
:
The obvious functor C ⥤ W.Localization
Instances For
def
CategoryTheory.Localization.Construction.wIso
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(w : X ⟶ Y)
(hw : W X Y w)
:
(CategoryTheory.MorphismProperty.Q W).obj X ≅ (CategoryTheory.MorphismProperty.Q W).obj Y
The isomorphism in W.Localization associated to a morphism w in W
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Localization.Construction.winv
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(w : X ⟶ Y)
(hw : W X Y w)
:
(CategoryTheory.MorphismProperty.Q W).obj Y ⟶ (CategoryTheory.MorphismProperty.Q W).obj X
The formal inverse in W.Localization of a morphism w in W.
Instances For
@[simp]
theorem
CategoryTheory.Localization.Construction.liftToPathCategory_obj
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
{W : CategoryTheory.MorphismProperty C}
{D : Type uD}
[CategoryTheory.Category.{uD', uD} D]
(G : CategoryTheory.Functor C D)
(hG : CategoryTheory.MorphismProperty.IsInvertedBy W G)
(X : CategoryTheory.Paths (CategoryTheory.Localization.Construction.LocQuiver W))
:
(CategoryTheory.Localization.Construction.liftToPathCategory G hG).obj X = G.obj X.obj
@[simp]
theorem
CategoryTheory.Localization.Construction.liftToPathCategory_map
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
{W : CategoryTheory.MorphismProperty C}
{D : Type uD}
[CategoryTheory.Category.{uD', uD} D]
(G : CategoryTheory.Functor C D)
(hG : CategoryTheory.MorphismProperty.IsInvertedBy W G)
:
∀ {X Y : CategoryTheory.Paths (CategoryTheory.Localization.Construction.LocQuiver W)} (f : X ⟶ Y),
(CategoryTheory.Localization.Construction.liftToPathCategory G hG).map f = CategoryTheory.composePath
(Prefunctor.mapPath
{ obj := fun X => G.obj X.obj,
map := fun {X Y} a => Sum.rec (fun val => G.map val) (fun val => CategoryTheory.inv (G.map ↑val)) a }
f)
def
CategoryTheory.Localization.Construction.liftToPathCategory
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
{W : CategoryTheory.MorphismProperty C}
{D : Type uD}
[CategoryTheory.Category.{uD', uD} D]
(G : CategoryTheory.Functor C D)
(hG : CategoryTheory.MorphismProperty.IsInvertedBy W G)
:
The lifting of a functor to the path category of LocQuiver W
Instances For
@[simp]
theorem
CategoryTheory.Localization.Construction.lift_obj
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
{W : CategoryTheory.MorphismProperty C}
{D : Type uD}
[CategoryTheory.Category.{uD', uD} D]
(G : CategoryTheory.Functor C D)
(hG : CategoryTheory.MorphismProperty.IsInvertedBy W G)
(a : CategoryTheory.Quotient (CategoryTheory.Localization.Construction.relations W))
:
(CategoryTheory.Localization.Construction.lift G hG).obj a = G.obj a.as.obj
@[simp]
theorem
CategoryTheory.Localization.Construction.lift_map
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
{W : CategoryTheory.MorphismProperty C}
{D : Type uD}
[CategoryTheory.Category.{uD', uD} D]
(G : CategoryTheory.Functor C D)
(hG : CategoryTheory.MorphismProperty.IsInvertedBy W G)
(a : CategoryTheory.Quotient (CategoryTheory.Localization.Construction.relations W))
(b : CategoryTheory.Quotient (CategoryTheory.Localization.Construction.relations W))
(hf : a ⟶ b)
:
(CategoryTheory.Localization.Construction.lift G hG).map hf = Quot.liftOn hf
(fun f =>
CategoryTheory.composePath
(Prefunctor.mapPath
{ obj := fun X => G.obj X.obj,
map := fun {X Y} a => Sum.rec (fun val => G.map val) (fun val => CategoryTheory.inv (G.map ↑val)) a }
f))
(_ :
∀ (a b : a.as ⟶ b.as),
CategoryTheory.Quotient.CompClosure (CategoryTheory.Localization.Construction.relations W) a b →
(fun f => (CategoryTheory.Localization.Construction.liftToPathCategory G hG).map f) a = (fun f => (CategoryTheory.Localization.Construction.liftToPathCategory G hG).map f) b)
def
CategoryTheory.Localization.Construction.lift
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
{W : CategoryTheory.MorphismProperty C}
{D : Type uD}
[CategoryTheory.Category.{uD', uD} D]
(G : CategoryTheory.Functor C D)
(hG : CategoryTheory.MorphismProperty.IsInvertedBy W G)
:
The lifting of a functor C ⥤ D inverting W as a functor W.Localization ⥤ D
Instances For
@[simp]
theorem
CategoryTheory.Localization.Construction.fac
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
{W : CategoryTheory.MorphismProperty C}
{D : Type uD}
[CategoryTheory.Category.{uD', uD} D]
(G : CategoryTheory.Functor C D)
(hG : CategoryTheory.MorphismProperty.IsInvertedBy W G)
:
theorem
CategoryTheory.Localization.Construction.uniq
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
{W : CategoryTheory.MorphismProperty C}
{D : Type uD}
[CategoryTheory.Category.{uD', uD} D]
(G₁ : CategoryTheory.Functor (CategoryTheory.MorphismProperty.Localization W) D)
(G₂ : CategoryTheory.Functor (CategoryTheory.MorphismProperty.Localization W) D)
(h : CategoryTheory.Functor.comp (CategoryTheory.MorphismProperty.Q W) G₁ = CategoryTheory.Functor.comp (CategoryTheory.MorphismProperty.Q W) G₂)
:
G₁ = G₂
@[simp]
theorem
CategoryTheory.Localization.Construction.objEquiv_apply
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
:
∀ (a : C), ↑(CategoryTheory.Localization.Construction.objEquiv W) a = (CategoryTheory.MorphismProperty.Q W).obj a
@[simp]
theorem
CategoryTheory.Localization.Construction.objEquiv_symm_apply
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
(X : CategoryTheory.MorphismProperty.Localization W)
:
↑(CategoryTheory.Localization.Construction.objEquiv W).symm X = X.as.obj
def
CategoryTheory.Localization.Construction.objEquiv
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
:
The canonical bijection between objects in a category and its
localization with respect to a morphism_property W
Instances For
theorem
CategoryTheory.Localization.Construction.morphismProperty_is_top
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
{W : CategoryTheory.MorphismProperty C}
(P : CategoryTheory.MorphismProperty (CategoryTheory.MorphismProperty.Localization W))
(hP₁ : ⦃X Y : C⦄ →
(f : X ⟶ Y) →
P ((CategoryTheory.MorphismProperty.Q W).obj X) ((CategoryTheory.MorphismProperty.Q W).obj Y)
((CategoryTheory.MorphismProperty.Q W).map f))
(hP₂ : ⦃X Y : C⦄ →
(w : X ⟶ Y) →
(hw : W X Y w) →
P ((CategoryTheory.MorphismProperty.Q W).obj Y) ((CategoryTheory.MorphismProperty.Q W).obj X)
(CategoryTheory.Localization.Construction.winv w hw))
(hP₃ : CategoryTheory.MorphismProperty.StableUnderComposition P)
:
A MorphismProperty in W.Localization is satisfied by all
morphisms in the localized category if it contains the image of the
morphisms in the original category, the inverses of the morphisms
in W and if it is stable under composition
theorem
CategoryTheory.Localization.Construction.morphismProperty_is_top'
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
{W : CategoryTheory.MorphismProperty C}
(P : CategoryTheory.MorphismProperty (CategoryTheory.MorphismProperty.Localization W))
(hP₁ : ⦃X Y : C⦄ →
(f : X ⟶ Y) →
P ((CategoryTheory.MorphismProperty.Q W).obj X) ((CategoryTheory.MorphismProperty.Q W).obj Y)
((CategoryTheory.MorphismProperty.Q W).map f))
(hP₂ : ⦃X Y : CategoryTheory.MorphismProperty.Localization W⦄ → (e : X ≅ Y) → P X Y e.hom → P Y X e.inv)
(hP₃ : CategoryTheory.MorphismProperty.StableUnderComposition P)
:
A MorphismProperty in W.Localization is satisfied by all
morphisms in the localized category if it contains the image of the
morphisms in the original category, if is stable under composition
and if the property is stable by passing to inverses.
def
CategoryTheory.Localization.Construction.NatTransExtension.app
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
{W : CategoryTheory.MorphismProperty C}
{D : Type uD}
[CategoryTheory.Category.{uD', uD} D]
{F₁ : CategoryTheory.Functor (CategoryTheory.MorphismProperty.Localization W) D}
{F₂ : CategoryTheory.Functor (CategoryTheory.MorphismProperty.Localization W) D}
(τ : CategoryTheory.Functor.comp (CategoryTheory.MorphismProperty.Q W) F₁ ⟶ CategoryTheory.Functor.comp (CategoryTheory.MorphismProperty.Q W) F₂)
(X : CategoryTheory.MorphismProperty.Localization W)
:
F₁.obj X ⟶ F₂.obj X
If F₁ and F₂ are functors W.Localization ⥤ D and if we have
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂, we shall define a natural transformation F₁ ⟶ F₂.
This is the app field of this natural transformation.
Instances For
@[simp]
theorem
CategoryTheory.Localization.Construction.NatTransExtension.app_eq
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
{W : CategoryTheory.MorphismProperty C}
{D : Type uD}
[CategoryTheory.Category.{uD', uD} D]
{F₁ : CategoryTheory.Functor (CategoryTheory.MorphismProperty.Localization W) D}
{F₂ : CategoryTheory.Functor (CategoryTheory.MorphismProperty.Localization W) D}
(τ : CategoryTheory.Functor.comp (CategoryTheory.MorphismProperty.Q W) F₁ ⟶ CategoryTheory.Functor.comp (CategoryTheory.MorphismProperty.Q W) F₂)
(X : C)
:
CategoryTheory.Localization.Construction.NatTransExtension.app τ ((CategoryTheory.MorphismProperty.Q W).obj X) = τ.app X
@[simp]
theorem
CategoryTheory.Localization.Construction.natTransExtension_app
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
{W : CategoryTheory.MorphismProperty C}
{D : Type uD}
[CategoryTheory.Category.{uD', uD} D]
{F₁ : CategoryTheory.Functor (CategoryTheory.MorphismProperty.Localization W) D}
{F₂ : CategoryTheory.Functor (CategoryTheory.MorphismProperty.Localization W) D}
(τ : CategoryTheory.Functor.comp (CategoryTheory.MorphismProperty.Q W) F₁ ⟶ CategoryTheory.Functor.comp (CategoryTheory.MorphismProperty.Q W) F₂)
(X : CategoryTheory.MorphismProperty.Localization W)
:
def
CategoryTheory.Localization.Construction.natTransExtension
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
{W : CategoryTheory.MorphismProperty C}
{D : Type uD}
[CategoryTheory.Category.{uD', uD} D]
{F₁ : CategoryTheory.Functor (CategoryTheory.MorphismProperty.Localization W) D}
{F₂ : CategoryTheory.Functor (CategoryTheory.MorphismProperty.Localization W) D}
(τ : CategoryTheory.Functor.comp (CategoryTheory.MorphismProperty.Q W) F₁ ⟶ CategoryTheory.Functor.comp (CategoryTheory.MorphismProperty.Q W) F₂)
:
F₁ ⟶ F₂
If F₁ and F₂ are functors W.Localization ⥤ D, a natural transformation F₁ ⟶ F₂
can be obtained from a natural transformation W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂.
Instances For
@[simp]
theorem
CategoryTheory.Localization.Construction.natTransExtension_hcomp
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
{W : CategoryTheory.MorphismProperty C}
{D : Type uD}
[CategoryTheory.Category.{uD', uD} D]
{F : CategoryTheory.Functor (CategoryTheory.MorphismProperty.Localization W) D}
{G : CategoryTheory.Functor (CategoryTheory.MorphismProperty.Localization W) D}
(τ : CategoryTheory.Functor.comp (CategoryTheory.MorphismProperty.Q W) F ⟶ CategoryTheory.Functor.comp (CategoryTheory.MorphismProperty.Q W) G)
:
theorem
CategoryTheory.Localization.Construction.natTrans_hcomp_injective
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
{W : CategoryTheory.MorphismProperty C}
{D : Type uD}
[CategoryTheory.Category.{uD', uD} D]
{F : CategoryTheory.Functor (CategoryTheory.MorphismProperty.Localization W) D}
{G : CategoryTheory.Functor (CategoryTheory.MorphismProperty.Localization W) D}
{τ₁ : F ⟶ G}
{τ₂ : F ⟶ G}
(h : CategoryTheory.CategoryStruct.id (CategoryTheory.MorphismProperty.Q W) ◫ τ₁ = CategoryTheory.CategoryStruct.id (CategoryTheory.MorphismProperty.Q W) ◫ τ₂)
:
τ₁ = τ₂
@[simp]
theorem
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_map_app
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
(D : Type uD)
[CategoryTheory.Category.{uD', uD} D]
:
∀ {X Y : CategoryTheory.Functor (CategoryTheory.MorphismProperty.Localization W) D} (f : X ⟶ Y) (X_1 : C),
((CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor W D).map f).app X_1 = f.app ((CategoryTheory.MorphismProperty.Q W).obj X_1)
@[simp]
theorem
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_obj_obj_map
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
(D : Type uD)
[CategoryTheory.Category.{uD', uD} D]
(X : CategoryTheory.Functor (CategoryTheory.MorphismProperty.Localization W) D)
:
∀ {X Y : C} (f : X ⟶ Y),
((CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor W D).obj X).obj.map f = X.map ((CategoryTheory.MorphismProperty.Q W).map f)
@[simp]
theorem
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_obj_obj_obj
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
(D : Type uD)
[CategoryTheory.Category.{uD', uD} D]
(X : CategoryTheory.Functor (CategoryTheory.MorphismProperty.Localization W) D)
(X : C)
:
((CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor W D).obj X).obj.obj X = X.obj ((CategoryTheory.MorphismProperty.Q W).obj X)
def
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
(D : Type uD)
[CategoryTheory.Category.{uD', uD} D]
:
The functor (W.Localization ⥤ D) ⥤ (W.FunctorsInverting D) induced by the
composition with W.Q : C ⥤ W.Localization.
Instances For
@[simp]
theorem
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_map
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
(D : Type uD)
[CategoryTheory.Category.{uD', uD} D]
(G : CategoryTheory.MorphismProperty.FunctorsInverting W D)
(a : CategoryTheory.Quotient (CategoryTheory.Localization.Construction.relations W))
(b : CategoryTheory.Quotient (CategoryTheory.Localization.Construction.relations W))
(hf : a ⟶ b)
:
((CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse W D).obj G).map hf = Quot.liftOn hf
(fun f =>
CategoryTheory.composePath
(Prefunctor.mapPath
{ obj := fun X => G.obj.obj X.obj,
map := fun {X Y} a =>
Sum.rec (fun val => G.obj.map val) (fun val => CategoryTheory.inv (G.obj.map ↑val)) a }
f))
(_ :
∀ (a b : a.as ⟶ b.as),
CategoryTheory.Quotient.CompClosure (CategoryTheory.Localization.Construction.relations W) a b →
(fun f =>
(CategoryTheory.Localization.Construction.liftToPathCategory G.obj
(_ : CategoryTheory.MorphismProperty.IsInvertedBy W G.obj)).map
f)
a = (fun f =>
(CategoryTheory.Localization.Construction.liftToPathCategory G.obj
(_ : CategoryTheory.MorphismProperty.IsInvertedBy W G.obj)).map
f)
b)
@[simp]
theorem
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_map_app
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
(D : Type uD)
[CategoryTheory.Category.{uD', uD} D]
:
∀ {X Y : CategoryTheory.MorphismProperty.FunctorsInverting W D} (τ : X ⟶ Y)
(X_1 : CategoryTheory.MorphismProperty.Localization W),
((CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse W D).map τ).app X_1 = CategoryTheory.Localization.Construction.NatTransExtension.app
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom
(_ :
CategoryTheory.Functor.comp (CategoryTheory.MorphismProperty.Q W)
((fun G =>
CategoryTheory.Localization.Construction.lift G.obj
(_ : CategoryTheory.MorphismProperty.IsInvertedBy W G.obj))
X) = X.obj))
(CategoryTheory.CategoryStruct.comp τ
(CategoryTheory.eqToHom
(_ :
Y.obj = CategoryTheory.Functor.comp (CategoryTheory.MorphismProperty.Q W)
((fun G =>
CategoryTheory.Localization.Construction.lift G.obj
(_ : CategoryTheory.MorphismProperty.IsInvertedBy W G.obj))
Y)))))
X_1
@[simp]
theorem
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_obj
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
(D : Type uD)
[CategoryTheory.Category.{uD', uD} D]
(G : CategoryTheory.MorphismProperty.FunctorsInverting W D)
(a : CategoryTheory.Quotient (CategoryTheory.Localization.Construction.relations W))
:
((CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse W D).obj G).obj a = G.obj.obj a.as.obj
def
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
(D : Type uD)
[CategoryTheory.Category.{uD', uD} D]
:
The function (W.FunctorsInverting D) ⥤ (W.Localization ⥤ D) induced by
Construction.lift.
Instances For
@[simp]
theorem
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso_inv
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
(D : Type uD)
[CategoryTheory.Category.{uD', uD} D]
:
(CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso W D).inv = CategoryTheory.eqToHom
(_ :
CategoryTheory.Functor.comp (CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor W D)
(CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse W D) = CategoryTheory.Functor.id (CategoryTheory.Functor (CategoryTheory.MorphismProperty.Localization W) D))
@[simp]
theorem
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso_hom
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
(D : Type uD)
[CategoryTheory.Category.{uD', uD} D]
:
(CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso W D).hom = CategoryTheory.eqToHom
(_ :
CategoryTheory.Functor.id (CategoryTheory.Functor (CategoryTheory.MorphismProperty.Localization W) D) = CategoryTheory.Functor.comp (CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor W D)
(CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse W D))
def
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
(D : Type uD)
[CategoryTheory.Category.{uD', uD} D]
:
The unit isomorphism of the equivalence of categories whiskeringLeftEquivalence W D.
Instances For
@[simp]
theorem
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso_inv
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
(D : Type uD)
[CategoryTheory.Category.{uD', uD} D]
:
(CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso W D).inv = CategoryTheory.eqToHom
(_ :
CategoryTheory.Functor.id (CategoryTheory.MorphismProperty.FunctorsInverting W D) = CategoryTheory.Functor.comp (CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse W D)
(CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor W D))
@[simp]
theorem
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso_hom
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
(D : Type uD)
[CategoryTheory.Category.{uD', uD} D]
:
(CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso W D).hom = CategoryTheory.eqToHom
(_ :
CategoryTheory.Functor.comp (CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse W D)
(CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor W D) = CategoryTheory.Functor.id (CategoryTheory.MorphismProperty.FunctorsInverting W D))
def
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
(D : Type uD)
[CategoryTheory.Category.{uD', uD} D]
:
The counit isomorphism of the equivalence of categories WhiskeringLeftEquivalence W D.
Instances For
def
CategoryTheory.Localization.Construction.whiskeringLeftEquivalence
{C : Type uC}
[CategoryTheory.Category.{uC', uC} C]
(W : CategoryTheory.MorphismProperty C)
(D : Type uD)
[CategoryTheory.Category.{uD', uD} D]
:
The equivalence of categories (W.localization ⥤ D) ≌ (W.FunctorsInverting D)
induced by the composition with W.Q : C ⥤ W.localization.