Displayed Category Of A Functor

Given a type family F : C → Type* on a category C we then define the displayed category Display F.

For a functor P : E ⥤ C, we define the structure BasedLift f src tgt as the type of lifts in E of a given morphism f : c ⟶ d in C which have a fixed source src and a fixed target tgt in the fibers of c and d respectively. We call the elements of BasedLift f src tgt based-lifts of f with source src and target tgt.

We also provide various useful constructors for based-lifts:

• BasedLift.tauto regards a morphism g of the domain category E as a tautological based-lift of its image P.map g.
• BasedLift.id and BasedLift.comp provide the identity and composition of based-lifts, respectively.
• We can cast a based-lift along an equality of the base morphisms using the equivalence BasedLift.cast.

We provide the following notations:

• X ⟶[f] Y for DisplayStruct.HomOver f x y
• f ≫ₗ g for DisplayStruct.comp_over f g

We show that for a functor P, the type BasedLift P induces a display category structure on the fiber family fun c => P⁻¹ c.

def CategoryTheory.fiberCast {C : Type u_1} (F : C → Type u_2) {I : C} {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.fiberCast F w X = w ▸ X

def CategoryTheory.eqToHomMap {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {I : C} {I' : C} {J : C} {J' : C} (w : I = I') (w' : J = J') (f : I ⟶ J) : 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.eqToHomMap w w' f = w' ▸ w ▸ f

@[simp]

def CategoryTheory.eqToHomMapId {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {I : C} {I' : C} (w : I = I') : w ▸ CategoryTheory.CategoryStruct.id I = CategoryTheory.CategoryStruct.id I'

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.eqToHomMap_naturality {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {I : C} {I' : C} {J : C} {J' : C} {w : I = I'} {w' : J = J'} (f : I ⟶ J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom w) (CategoryTheory.eqToHomMap w w' f) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom w')

@[simp]

theorem CategoryTheory.fiber_cast_trans {C : Type u_1} (F : C → Type u_2) {I : C} {I' : C} {I'' : C} (X : F I) {w : I = I'} {w' : I' = I''} {w'' : I = I''} : w' ▸ w ▸ X = w'' ▸ X

theorem CategoryTheory.fiber_cast_cast {C : Type u_1} (F : C → Type u_2) {I : C} {I' : C} (X : F I) {w : I = I'} {w' : I' = I} : w' ▸ w ▸ X = X

class CategoryTheory.DisplayStruct {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (F : C → Type u_2) : Type (max (max (max u_1 u_2) (u_3 + 1)) u_4)

• HomOver : {I J : C} → (I ⟶ J) → F I → F J → Type u_3

  The type of morphisms indexed over morphisms of C.

• id_over : {I : C} → (X : F I) → X ⟶[CategoryTheory.CategoryStruct.id I] X

  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 ⟶[CategoryTheory.CategoryStruct.comp f₁ f₂] Z

  Composition of morphisms overlying composition of morphisms of C.

def CategoryTheory.«term_⟶[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.«term𝟙ₗ» : Lean.ParserDescr

Equations

• CategoryTheory.«term𝟙ₗ» = Lean.ParserDescr.node `CategoryTheory.term𝟙ₗ 1024 (Lean.ParserDescr.symbol " 𝟙ₗ ")

def CategoryTheory.«term_≫ₗ_» : Lean.TrailingParserDescr

Equations

• CategoryTheory.«term_≫ₗ_» = Lean.ParserDescr.trailingNode `CategoryTheory.term_≫ₗ_ 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≫ₗ ") (Lean.ParserDescr.cat `term 80))

class CategoryTheory.DisplayStruct.CastEq {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.DisplayStruct F] {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y) (g' : X ⟶[f'] Y) : Prop

• base_eq : f = f'
• cast_eq : ⋯ ▸ g = g'

theorem CategoryTheory.DisplayStruct.CastEq.base_eq {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.DisplayStruct F] {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y) (g' : X ⟶[f'] Y) [self : CategoryTheory.DisplayStruct.CastEq g g'] : f = f'

theorem CategoryTheory.DisplayStruct.CastEq.cast_eq {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.DisplayStruct F] {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : F I} {Y : F J} {g : X ⟶[f] Y} {g' : X ⟶[f'] Y} [self : CategoryTheory.DisplayStruct.CastEq g g'] : ⋯ ▸ g = g'

def CategoryTheory.«term_=▸=_» : Lean.TrailingParserDescr

Equations

• CategoryTheory.«term_=▸=_» = Lean.ParserDescr.trailingNode `CategoryTheory.term_=▸=_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " =▸= ") (Lean.ParserDescr.cat `term 50))

class CategoryTheory.Display {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (F : C → Type u_2) extends CategoryTheory.DisplayStruct : Type (max (max (max u_1 u_2) u_3) (u_4 + 1))

• HomOver : {I J : C} → (I ⟶ J) → F I → F J → Type u_4
• id_over : {I : C} → (X : F I) → X ⟶[CategoryTheory.CategoryStruct.id I] X
• 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 ⟶[CategoryTheory.CategoryStruct.comp f₁ f₂] Z
• id_comp_cast : ∀ {I J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y), CategoryTheory.DisplayStruct.CastEq (CategoryTheory.DisplayStruct.comp_over ( 𝟙ₗ X) g) g
• comp_id_cast : ∀ {I J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y), CategoryTheory.DisplayStruct.CastEq (CategoryTheory.DisplayStruct.comp_over g ( 𝟙ₗ Y)) g
• 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), CategoryTheory.DisplayStruct.CastEq (CategoryTheory.DisplayStruct.comp_over (CategoryTheory.DisplayStruct.comp_over g₁ g₂) g₃) (CategoryTheory.DisplayStruct.comp_over g₁ (CategoryTheory.DisplayStruct.comp_over g₂ g₃))

@[simp]

theorem CategoryTheory.Display.id_comp_cast {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [self : CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y) : CategoryTheory.DisplayStruct.CastEq (CategoryTheory.DisplayStruct.comp_over ( 𝟙ₗ X) g) g

@[simp]

theorem CategoryTheory.Display.comp_id_cast {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [self : CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y) : CategoryTheory.DisplayStruct.CastEq (CategoryTheory.DisplayStruct.comp_over g ( 𝟙ₗ Y)) g

@[simp]

theorem CategoryTheory.Display.assoc_cast {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [self : CategoryTheory.Display F] {I : C} {J : C} {K : C} {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) : CategoryTheory.DisplayStruct.CastEq (CategoryTheory.DisplayStruct.comp_over (CategoryTheory.DisplayStruct.comp_over g₁ g₂) g₃) (CategoryTheory.DisplayStruct.comp_over g₁ (CategoryTheory.DisplayStruct.comp_over g₂ g₃))

def CategoryTheory.HomOver.cast {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : F I} {Y : F J} (w : f = f') (g : X ⟶[f] Y) : X ⟶[f'] Y

Equations

• CategoryTheory.HomOver.cast w g = w ▸ g

@[simp]

theorem CategoryTheory.HomOver.cast_trans {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {f'' : I ⟶ J} {X : F I} {Y : F J} {w : f = f'} {w' : f' = f''} (g : X ⟶[f] Y) : w' ▸ w ▸ g = ⋯ ▸ g

theorem CategoryTheory.HomOver.cast_unique {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : F I} {Y : F J} {w : f = f'} {w' : f = f'} (g : X ⟶[f] Y) : w ▸ g = w' ▸ g

theorem CategoryTheory.HomOver.cast_cast {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : F I} {Y : F J} (w : f = f') (w' : f' = f) (g : X ⟶[f'] Y) : ⋯ ▸ ⋯ ▸ g = g

theorem CategoryTheory.HomOver.comp_id_eq_cast_id_comp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y) : CategoryTheory.DisplayStruct.CastEq (CategoryTheory.DisplayStruct.comp_over g ( 𝟙ₗ Y)) (CategoryTheory.DisplayStruct.comp_over ( 𝟙ₗ X) g)

def CategoryTheory.HomOver.eqToHom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {I' : C} (w : I = I') (X : F I) : X ⟶[CategoryTheory.eqToHom w] w ▸ X

EqToHom w X is a hom-over eqToHom w from X to w ▸ X.

Equations

• CategoryTheory.HomOver.eqToHom w X = w ▸ 𝟙ₗ X

def CategoryTheory.HomOver.eqToHomMap {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {I' : C} {J' : C} (w : I = I') (w' : J = J') {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y) : (w ▸ X) ⟶[CategoryTheory.eqToHomMap w w' f] w' ▸ Y

Equations

• CategoryTheory.HomOver.eqToHomMap w w' g = w ▸ w' ▸ g

def CategoryTheory.HomOver.eqToHomMapId {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {I' : C} (w : I = I') {X : F I} {Y : F I} (g : X ⟶[CategoryTheory.CategoryStruct.id I] Y) : (w ▸ X) ⟶[CategoryTheory.CategoryStruct.id I'] w ▸ Y

Equations

• CategoryTheory.HomOver.eqToHomMapId w g = w ▸ g

theorem CategoryTheory.HomOver.eqToHom_naturality {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {I' : C} {J' : C} {X : F I} {Y : F J} (w : I = I') (w' : J = J') (f : I ⟶ J) (g : X ⟶[f] Y) : CategoryTheory.DisplayStruct.comp_over g (CategoryTheory.HomOver.eqToHom w' Y) = CategoryTheory.HomOver.cast ⋯ (CategoryTheory.DisplayStruct.comp_over (CategoryTheory.HomOver.eqToHom w X) (CategoryTheory.HomOver.eqToHomMap w w' g))

@[simp]

theorem CategoryTheory.HomOver.castEquiv_symm_apply {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : F I} {Y : F J} (w : f = f') (g : X ⟶[f'] Y) : (CategoryTheory.HomOver.castEquiv w).symm g = ⋯ ▸ g

@[simp]

theorem CategoryTheory.HomOver.castEquiv_apply {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : F I} {Y : F J} (w : f = f') (g : X ⟶[f] Y) : (CategoryTheory.HomOver.castEquiv w) g = w ▸ g

def CategoryTheory.HomOver.castEquiv {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : F I} {Y : F J} (w : f = f') : (X ⟶[f] Y) ≃ X ⟶[f'] Y

Equations

• CategoryTheory.HomOver.castEquiv w = { toFun := fun (g : X ⟶[f] Y) => w ▸ g, invFun := fun (g : X ⟶[f'] Y) => ⋯ ▸ g, left_inv := ⋯, right_inv := ⋯ }