Displayed category #
Given a type family F : C → Type* on a category C we define the type class Displayed F
of displayed categories over F. A displayed category structure associates to each morphism f
in C and terms X : F I and Y : F J a type HomOver f X Y.
We think of F I as the Fiber over I, and we think of HomOver f X Y as the type of morphisms
lying over f starting from X and ending at Y. The data of a displayed category structure
also provides the dependent operations of identity and composition for HomOver.
Finally, the modified laws of associativity and unitality hold dependently over the associativity
and unitality equalities in C.
Main declarations #
Our main construction is the displayed category of a functor. Given a functor P : E ⥤ C, the
associated displayed category on the fiber family fun I => P⁻¹ I is provided by the instance
Functor.display. Here HomOver f X Y is given by the type BasedLift f src tgt carrying data
witnessing morphisms in E starting from src and ending at tgt and are mapped to f under P.
There is another displayed structure EBasedLift associated to a functor P : E ⥤ C which is
defined in terms of the displayed family of "fat" fibers, namely fun I => P⁻¹ᵉ I where P⁻¹ᵉ I
is the fibers of P at J for all J isomorphic to I. The type EBasedLift f src tgt is the
type of morphisms in E starting from src and ending at tgt and are mapped, up to the specified
isomorphisms of src and tgt, to f under P.
We also provide various useful constructors for based-lifts:
BasedLift.tautoregards a morphismgof the domain categoryEas a tautological based-lift of its imageP.map g.BasedLift.idandBasedLift.compprovide the identity and composition of based-lifts, respectively.BasedLift.castcasts a based-lift along an equality of the base morphisms using the equivalenceBasedLift.cast.
Notation #
We provide the following notations:
X ⟶[f] YforDisplayedStruct.HomOver f x yf ≫ₒ gforDisplayedStruct.comp_over f g𝟙ₒ XforDisplayedStruct.id_over
def
CategoryTheory.eqToHom.map
{C : Type u₁}
[Category.{v₁, u₁} C]
{I I' J J' : C}
(w : I = I')
(w' : J = J')
(f : I ⟶ J)
:
Transporting a morphism f : I ⟶ J along equalities w : I = I' and w' : J = J'.
Note: It might be a good idea to add this to eqToHom file.
Equations
- CategoryTheory.eqToHom.map w w' f = w' ▸ w ▸ f
Instances For
@[simp]
@[simp]
theorem
CategoryTheory.eqToHom.map_naturality
{C : Type u₁}
[Category.{v₁, u₁} C]
{I I' J J' : C}
{w : I = I'}
{w' : J = J'}
(f : I ⟶ J)
:
The diagram below commutes:
I --eqToHom w --> J
| |
f | | eqToHom.map w w' f
v v
I' --eqToHom w'-> J'
def
CategoryTheory.Fiber.cast
{C : Type u₁}
(F : C → Type u₂)
{I I' : C}
(w : I = I')
(X : F I)
:
F I'
Cast an element of a Fiber along an equality of the base objects.
Equations
- CategoryTheory.Fiber.cast F w X = w ▸ X
Instances For
theorem
CategoryTheory.Fiber.cast_cast
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : C → Type u₂)
{I I' : C}
(X : F I)
{w : I = I'}
{w' : I' = I}
:
class
CategoryTheory.DisplayedStruct
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : C → Type u₂)
:
Type (max (max (max u₁ u₂) v₁) (v₂ + 1))
The type of morphisms indexed over morphisms of
C.The identity morphism overlying the identity morphism of
C.- comp_over {I J K : C} {f₁ : I ⟶ J} {f₂ : J ⟶ K} {X : F I} {Y : F J} {Z : F K} : (X ⟶[f₁] Y) → (Y ⟶[f₂] Z) → X ⟶[CategoryStruct.comp f₁ f₂] Z
Composition of morphisms overlying composition of morphisms of
C.
Instances
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- CategoryTheory.«term𝟙ₒ» = Lean.ParserDescr.node `CategoryTheory.«term𝟙ₒ» 1024 (Lean.ParserDescr.symbol "𝟙ₒ")
Instances For
Equations
- CategoryTheory.«term_≫ₒ_» = Lean.ParserDescr.trailingNode `CategoryTheory.«term_≫ₒ_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≫ₒ ") (Lean.ParserDescr.cat `term 80))
Instances For
class
CategoryTheory.Displayed
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : C → Type u₂)
extends CategoryTheory.DisplayedStruct F :
Type (max (max (max (u_1 + 1) u₁) u₂) v₁)
- assoc_cast {I J K L : C} {f₁ : I ⟶ J} {f₂ : J ⟶ K} {f₃ : K ⟶ L} {X : F I} {Y : F J} {Z : F K} {W : F L} (g₁ : X ⟶[f₁] Y) (g₂ : Y ⟶[f₂] Z) (g₃ : Z ⟶[f₃] W) : DisplayedStruct.comp_over (DisplayedStruct.comp_over g₁ g₂) g₃ = ⋯ ▸ DisplayedStruct.comp_over g₁ (DisplayedStruct.comp_over g₂ g₃)
Instances
def
CategoryTheory.Displayed.cast
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : C → Type u₂}
[Displayed F]
{I J : C}
{f f' : I ⟶ J}
{X : F I}
{Y : F J}
(w : f = f')
(g : X ⟶[f] Y)
:
Equations
- CategoryTheory.Displayed.cast w g = w ▸ g
Instances For
theorem
CategoryTheory.Displayed.cast_assoc_symm
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : C → Type u₂}
[Displayed F]
{I J K L : C}
{f₁ : I ⟶ J}
{f₂ : J ⟶ K}
{f₃ : K ⟶ L}
{X : F I}
{Y : F J}
{Z : F K}
{W : F L}
(g₁ : X ⟶[f₁] Y)
(g₂ : Y ⟶[f₂] Z)
(g₃ : Z ⟶[f₃] W)
:
⋯ ▸ DisplayedStruct.comp_over (DisplayedStruct.comp_over g₁ g₂) g₃ = DisplayedStruct.comp_over g₁ (DisplayedStruct.comp_over g₂ g₃)
@[simp]
theorem
CategoryTheory.Displayed.comp_id_eq_cast_id_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : C → Type u₂}
[Displayed F]
{I J : C}
{f : I ⟶ J}
{X : F I}
{Y : F J}
(g : X ⟶[f] Y)
:
def
CategoryTheory.Displayed.castToHomInv
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : C → Type u₂}
[Displayed F]
{I I' : C}
(w : I = I')
(X : F I)
:
Equations
- CategoryTheory.Displayed.castToHomInv w X = w ▸ 𝟙ₒ X
Instances For
def
CategoryTheory.Displayed.castToHomMap
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : C → Type u₂}
[Displayed F]
{I I' J J' : C}
(w : I = I')
(w' : J = J')
{f : I ⟶ J}
{X : F I}
{Y : F J}
(g : X ⟶[f] Y)
:
Equations
- CategoryTheory.Displayed.castToHomMap w w' g = w ▸ w' ▸ g
Instances For
def
CategoryTheory.Displayed.castToHomMapId
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : C → Type u₂}
[Displayed F]
{I I' : C}
(w : I = I')
{X Y : F I}
(g : X ⟶[CategoryStruct.id I] Y)
:
Equations
Instances For
theorem
CategoryTheory.Displayed.eqToHom_naturality
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : C → Type u₂}
[Displayed F]
{I I' J J' : C}
{X : F I}
{Y : F J}
(w : I = I')
(w' : J = J')
(f : I ⟶ J)
(g : X ⟶[f] Y)
:
DisplayedStruct.comp_over g (castToHom w' Y) = cast ⋯ (DisplayedStruct.comp_over (castToHom w X) (castToHomMap w w' g))
The displayed diagram
X --------g--------> Y
| |
eqToHom w X | | eqToHom w' Y
v v
w ▸ X -------------> w ▸ Y
eqToHom.map w w' g
commutes.
def
CategoryTheory.Displayed.castEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : C → Type u₂}
[Displayed F]
{I J : C}
{f f' : I ⟶ J}
{X : F I}
{Y : F J}
(w : f = f')
:
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- CategoryTheory.Displayed.Total.mk X = ⟨I, X⟩
Instances For
def
CategoryTheory.Displayed.Total.Hom.mk
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : C → Type u₂}
[Displayed F]
{I J : C}
{X : F I}
{Y : F J}
{f : I ⟶ J}
(g : X ⟶[f] Y)
:
Equations
- CategoryTheory.Displayed.Total.Hom.mk g = ⟨f, g⟩
Instances For
instance
CategoryTheory.Displayed.Total.categoryStruct
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : C → Type u₂}
[Displayed F]
:
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Displayed.Total.category
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : C → Type u₂}
[Displayed F]
:
Equations
- CategoryTheory.Displayed.Total.category = { toCategoryStruct := CategoryTheory.Displayed.Total.categoryStruct, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }
def
CategoryTheory.Displayed.Total.forget
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : C → Type u₂}
[Displayed F]
:
Equations
Instances For
structure
CategoryTheory.BasedLift
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{I J : C}
(f : I ⟶ J)
(X : P ⁻¹ I)
(Y : P ⁻¹ J)
:
Type u_2
The type of lifts of a given morphism in the base with fixed source and target in the Fibers of the domain and codomain respectively.
- over_eq : CategoryStruct.comp (P.map self.hom) (CategoryTheory.eqToHom ⋯) = CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f
Instances For
def
CategoryTheory.BasedLift'
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{I J : C}
(f : I ⟶ J)
(X : P ⁻¹ I)
(Y : P ⁻¹ J)
:
Type u_2
Equations
- One or more equations did not get rendered due to their size.
Instances For
structure
CategoryTheory.EBasedLift
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{I J : C}
(f : I ⟶ J)
(X : P ⁻¹ᵉ I)
(Y : P ⁻¹ᵉ J)
:
Type u_2
The structure of based-lifts up to an isomorphism of the domain objects in the base.
X -------------------------------> Y
_ -
| |
| |
v v
P.obj X --------> I ------> J ----> P.obj Y
≅ f ≅
Instances For
theorem
CategoryTheory.EBasedLift.over_eq_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{I J : C}
{f : I ⟶ J}
{X : P ⁻¹ᵉ I}
{Y : P ⁻¹ᵉ J}
(self : EBasedLift f X Y)
{Z : C}
(h : J ⟶ Z)
:
CategoryStruct.comp (P.map self.hom) (CategoryStruct.comp Y.iso.hom h) = CategoryStruct.comp X.iso.hom (CategoryStruct.comp f h)
@[simp]
theorem
CategoryTheory.BasedLift.over_eq'
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_2}
[Category.{u_3, u_2} E]
{P : Functor E C}
{I J : C}
{f : I ⟶ J}
{X : P ⁻¹ I}
{Y : P ⁻¹ J}
(g : BasedLift f X Y)
:
def
CategoryTheory.BasedLift.id
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_2}
[Category.{u_3, u_2} E]
{P : Functor E C}
{I : C}
(X : P ⁻¹ I)
:
BasedLift (CategoryStruct.id I) X X
The identity based-lift.
Equations
- CategoryTheory.BasedLift.id X = { hom := CategoryTheory.CategoryStruct.id ↑X, over_eq := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.BasedLift.id_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_2}
[Category.{u_3, u_2} E]
{P : Functor E C}
{I : C}
(X : P ⁻¹ I)
:
def
CategoryTheory.BasedLift.comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_2}
[Category.{u_3, u_2} E]
{P : Functor E C}
{I J K : C}
{f₁ : I ⟶ J}
{f₂ : J ⟶ K}
{X : P ⁻¹ I}
{Y : P ⁻¹ J}
{Z : P ⁻¹ K}
(g₁ : BasedLift f₁ X Y)
(g₂ : BasedLift f₂ Y Z)
:
BasedLift (CategoryStruct.comp f₁ f₂) X Z
The composition of based-lifts
Equations
- g₁.comp g₂ = { hom := CategoryTheory.CategoryStruct.comp g₁.hom g₂.hom, over_eq := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.BasedLift.comp_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_2}
[Category.{u_3, u_2} E]
{P : Functor E C}
{I J K : C}
{f₁ : I ⟶ J}
{f₂ : J ⟶ K}
{X : P ⁻¹ I}
{Y : P ⁻¹ J}
{Z : P ⁻¹ K}
(g₁ : BasedLift f₁ X Y)
(g₂ : BasedLift f₂ Y Z)
:
def
CategoryTheory.BasedLift.cast
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_2}
[Category.{u_3, u_2} E]
{P : Functor E C}
{I J : C}
{f f' : I ⟶ J}
{X : P ⁻¹ I}
{Y : P ⁻¹ J}
(w : f = f')
(g : BasedLift f X Y)
:
BasedLift f' X Y
Equations
- CategoryTheory.BasedLift.cast w g = { hom := g.hom, over_eq := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.EBasedLift.over_eq'
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{I J : C}
{f : I ⟶ J}
{X : P ⁻¹ᵉ I}
{Y : P ⁻¹ᵉ J}
(g : EBasedLift f X Y)
:
def
CategoryTheory.EBasedLift.id
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{I : C}
(X : P ⁻¹ᵉ I)
:
EBasedLift (CategoryStruct.id I) X X
Equations
- CategoryTheory.EBasedLift.id X = { hom := CategoryTheory.CategoryStruct.id X.obj, over_eq := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.EBasedLift.id_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{I : C}
(X : P ⁻¹ᵉ I)
:
def
CategoryTheory.EBasedLift.comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{I J K : C}
{f₁ : I ⟶ J}
{f₂ : J ⟶ K}
{X : P ⁻¹ᵉ I}
{Y : P ⁻¹ᵉ J}
{Z : P ⁻¹ᵉ K}
(g₁ : EBasedLift f₁ X Y)
(g₂ : EBasedLift f₂ Y Z)
:
EBasedLift (CategoryStruct.comp f₁ f₂) X Z
Equations
- g₁.comp g₂ = { hom := CategoryTheory.CategoryStruct.comp g₁.hom g₂.hom, over_eq := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.EBasedLift.comp_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{I J K : C}
{f₁ : I ⟶ J}
{f₂ : J ⟶ K}
{X : P ⁻¹ᵉ I}
{Y : P ⁻¹ᵉ J}
{Z : P ⁻¹ᵉ K}
(g₁ : EBasedLift f₁ X Y)
(g₂ : EBasedLift f₂ Y Z)
:
def
CategoryTheory.EBasedLift.cast
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{I J : C}
{f f' : I ⟶ J}
{X : P ⁻¹ᵉ I}
{Y : P ⁻¹ᵉ J}
(w : f = f')
(g : EBasedLift f X Y)
:
EBasedLift f' X Y
Equations
- CategoryTheory.EBasedLift.cast w g = { hom := g.hom, over_eq := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.EBasedLift.cast_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{I J : C}
{f f' : I ⟶ J}
{X : P ⁻¹ᵉ I}
{Y : P ⁻¹ᵉ J}
(w : f = f')
(g : EBasedLift f X Y)
:
instance
CategoryTheory.Functor.displayedStruct
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
(P : Functor E C)
:
DisplayedStruct fun (I : C) => P ⁻¹ I
The display structure DisplayedStruct P associated to a functor P : E ⥤ C.
This instance makes the displayed notations _ ⟶[f] _, _ ≫ₒ _ and 𝟙ₒ available for based-lifts.
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Functor.isodisplay
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
(P : Functor E C)
:
DisplayedStruct fun (I : C) => P ⁻¹ᵉ I
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.BasedLift.tauto
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{X Y : E}
(g : X ⟶ Y)
:
BasedLift.tauto regards a morphism g of the domain category E as a
based-lift of its image P g under functor P.
Equations
- CategoryTheory.BasedLift.tauto g = { hom := g, over_eq := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.BasedLift.tauto_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{X Y : E}
(g : X ⟶ Y)
:
theorem
CategoryTheory.BasedLift.tauto_over_base
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{X Y : E}
(f : P.obj X ⟶ P.obj Y)
(g : Fiber.tauto X ⟶[f] Fiber.tauto Y)
:
theorem
CategoryTheory.BasedLift.tauto_comp_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{X Y Z : E}
{g : X ⟶ Y}
{g' : Y ⟶ Z}
:
theorem
CategoryTheory.BasedLift.comp_tauto_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{X Y Z : E}
{f : P.obj X ⟶ P.obj Y}
{f' : Fiber.tauto X ⟶[f] Fiber.tauto Y}
{g : Y ⟶ Z}
:
instance
CategoryTheory.BasedLift.instCoeTautoBasedLift
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{X Y : E}
{g : X ⟶ Y}
:
CoeDep (X ⟶ Y) g (Fiber.tauto X ⟶[P.map g] Fiber.tauto Y)
A morphism of E coerced as a tautological based-lift.
Equations
@[simp]
theorem
CategoryTheory.BasedLift.instCoeTautoBasedLift_coe
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{X Y : E}
{g : X ⟶ Y}
:
theorem
CategoryTheory.BasedLift.eq_id_of_hom_eq_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{I : C}
{X : P ⁻¹ I}
{g : X ⟶[CategoryStruct.id I] X}
:
@[simp]
theorem
CategoryTheory.BasedLift.id_comp_cast
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{I J : C}
{f : I ⟶ J}
{X : P ⁻¹ I}
{Y : P ⁻¹ J}
{g : X ⟶[f] Y}
:
@[simp]
theorem
CategoryTheory.BasedLift.comp_id_cast
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{I J : C}
{f : I ⟶ J}
{X : P ⁻¹ I}
{Y : P ⁻¹ J}
{g : X ⟶[f] Y}
:
def
CategoryTheory.BasedLift.eqToHom
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{I : C}
{X Y : P ⁻¹ I}
(w : X = Y)
:
Equations
Instances For
def
CategoryTheory.BasedLift.eqToHom'
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{I : C}
{X Y : P ⁻¹ I}
(w : ↑X = ↑Y)
:
Equations
Instances For
def
CategoryTheory.EBasedLift.tauto
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{X Y : E}
(g : X ⟶ Y)
:
EBasedLift.tauto regards a morphism g of the domain category E as a
based-lift of its image P g under functor P.
Equations
- CategoryTheory.EBasedLift.tauto g = { hom := g, over_eq := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.EBasedLift.tauto_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{X Y : E}
(g : X ⟶ Y)
:
theorem
CategoryTheory.EBasedLift.tauto_over_base
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{X Y : E}
(f : P.obj X ⟶ P.obj Y)
(g : Fiber.tauto X ⟶[f] Fiber.tauto Y)
:
theorem
CategoryTheory.EBasedLift.tauto_comp_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{X Y Z : E}
{g : X ⟶ Y}
{g' : Y ⟶ Z}
:
theorem
CategoryTheory.EBasedLift.comp_tauto_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{X Y Z : E}
{f : P.obj X ⟶ P.obj Y}
{f' : EFiber.tauto X ⟶[f] EFiber.tauto Y}
{g : Y ⟶ Z}
:
instance
CategoryTheory.EBasedLift.instCoeTautoBasedLift
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{X Y : E}
{g : X ⟶ Y}
:
CoeDep (X ⟶ Y) g (EFiber.tauto X ⟶[P.map g] EFiber.tauto Y)
A morphism of E coerced as a tautological based-lift.
Equations
@[simp]
theorem
CategoryTheory.EBasedLift.instCoeTautoBasedLift_coe
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{X Y : E}
{g : X ⟶ Y}
:
theorem
CategoryTheory.EBasedLift.eq_id_of_hom_eq_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{I : C}
{X : P ⁻¹ᵉ I}
{g : X ⟶[CategoryStruct.id I] X}
:
@[simp]
theorem
CategoryTheory.EBasedLift.id_comp_cast
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{I J : C}
{f : I ⟶ J}
{X : P ⁻¹ᵉ I}
{Y : P ⁻¹ᵉ J}
{g : X ⟶[f] Y}
:
@[simp]
theorem
CategoryTheory.EBasedLift.comp_id_cast
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
{P : Functor E C}
{I J : C}
{f : I ⟶ J}
{X : P ⁻¹ᵉ I}
{Y : P ⁻¹ᵉ J}
{g : X ⟶[f] Y}
:
instance
CategoryTheory.Functor.display
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
(P : Functor E C)
:
The displayed category of a functor P : E ⥤ C.
Equations
- P.display = { toDisplayedStruct := P.displayedStruct, id_comp_cast := ⋯, comp_id_cast := ⋯, assoc_cast := ⋯ }
instance
CategoryTheory.Functor.edisplay
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u_1}
[Category.{u_2, u_1} E]
(P : Functor E C)
:
Equations
- P.edisplay = { toDisplayedStruct := P.isodisplay, id_comp_cast := ⋯, comp_id_cast := ⋯, assoc_cast := ⋯ }
structure
CategoryTheory.Displayed.Lift
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : C → Type u₂}
[Displayed F]
{I J : C}
(f : I ⟶ J)
(tgt : F J)
:
Type (max u_2 u₂)
The type Lift f tgt of a lift of f with the target tgt consists of an object src in
the Fiber of the domain of f and a based-lift of f starting at src and ending at tgt.
- src : F I
Instances For
structure
CategoryTheory.Displayed.CoLift
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : C → Type u₂}
[Displayed F]
{I J : C}
(f : I ⟶ J)
(src : F I)
:
Type (max u_2 u₂)
The type CoLift f src of a colift of f with the source src consists of an object tgt in
the Fiber of the codomain of f and a based-lift of f starting at src and ending at tgt.
- tgt : F J