Displayed category

Given a type family F : C → Type* on a category C we define the type class Display 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.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.

• BasedLift.cast casts a based-lift along an equality of the base morphisms using the equivalence BasedLift.cast.

Notation

We provide the following notations:

• X ⟶[f] Y for DisplayStruct.HomOver f x y

• f ≫ₒ g for DisplayStruct.comp_over f g

• 𝟙ₒ X for DisplayStruct.id_over

References

Benedikt Ahrens, Peter LeFanu Lumsdaine, Displayed Categories, Logical Methods in Computer Science 15 (1).

def CategoryTheory.eqToHom.map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} 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.eqToHom.map w w' f = w' ▸ w ▸ f

@[simp]

theorem CategoryTheory.eqToHom.map_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : C} {I' : C} (w : I = I') : w ▸ CategoryTheory.CategoryStruct.id I = CategoryTheory.CategoryStruct.id I'

@[simp]

theorem CategoryTheory.eqToHom.map_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} 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.eqToHom.map w w' f) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom w')

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 : 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.Fiber.cast F w X = w ▸ X

@[simp]

theorem CategoryTheory.Fiber.cast_trans {C : Type u₁} (F : C → Type u₂) {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₁} (F : C → Type u₂) {I : C} {I' : C} (X : F I) {w : I = I'} {w' : I' = I} : w' ▸ w ▸ X = X

class CategoryTheory.DisplayStruct {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : C → Type u₂) : Type (max (max (max u₁ u₂) v₁) (v₂ + 1))

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

  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.Display {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : C → Type u₂) extends CategoryTheory.DisplayStruct : Type (max (max (max (u_1 + 1) u₁) u₂) v₁)

• HomOver : {I J : C} → (I ⟶ J) → F I → F J → Type u_1
• 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.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.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.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₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [self : CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y) : CategoryTheory.DisplayStruct.comp_over (𝟙ₒ X) g = ⋯ ▸ g

@[simp]

theorem CategoryTheory.Display.comp_id_cast {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [self : CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y) : CategoryTheory.DisplayStruct.comp_over g (𝟙ₒ Y) = ⋯ ▸ g

@[simp]

theorem CategoryTheory.Display.assoc_cast {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [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.comp_over (CategoryTheory.DisplayStruct.comp_over g₁ g₂) g₃ = ⋯ ▸ CategoryTheory.DisplayStruct.comp_over g₁ (CategoryTheory.DisplayStruct.comp_over g₂ g₃)

def CategoryTheory.Display.cast {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [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.Display.cast w g = w ▸ g

@[simp]

theorem CategoryTheory.Display.cast_symm {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [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) (g' : X ⟶[f'] Y) : w ▸ g = g' ↔ g = ⋯ ▸ g'

theorem CategoryTheory.Display.cast_assoc_symm {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [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.comp_over (CategoryTheory.DisplayStruct.comp_over g₁ g₂) g₃ = CategoryTheory.DisplayStruct.comp_over g₁ (CategoryTheory.DisplayStruct.comp_over g₂ g₃)

@[simp]

theorem CategoryTheory.Display.cast_trans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [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.Display.cast_eq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [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

@[simp]

theorem CategoryTheory.Display.cast_cast {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [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

@[simp]

theorem CategoryTheory.Display.comp_id_eq_cast_id_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y) : CategoryTheory.DisplayStruct.comp_over g (𝟙ₒ Y) = CategoryTheory.Display.cast ⋯ (CategoryTheory.DisplayStruct.comp_over (𝟙ₒ X) g)

def CategoryTheory.Display.castToHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [CategoryTheory.Display F] {I : C} {I' : C} (w : I = I') (X : F I) : X ⟶[CategoryTheory.eqToHom w] w ▸ X

castToHom w X is a morphism from X to w ▸ X over eqToHom w.

Equations

• CategoryTheory.Display.castToHom w X = w ▸ 𝟙ₒ X

def CategoryTheory.Display.castToHomInv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [CategoryTheory.Display F] {I : C} {I' : C} (w : I = I') (X : F I) : (w ▸ X) ⟶[CategoryTheory.eqToHom ⋯] X

Equations

• CategoryTheory.Display.castToHomInv w X = w ▸ 𝟙ₒ X

def CategoryTheory.Display.castToHomMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [CategoryTheory.Display F] {I : C} {I' : C} {J : 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.eqToHom.map w w' f] w' ▸ Y

Equations

• CategoryTheory.Display.castToHomMap w w' g = w ▸ w' ▸ g

def CategoryTheory.Display.castToHomMapId {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [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.Display.castToHomMapId w g = w ▸ g

theorem CategoryTheory.Display.eqToHom_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [CategoryTheory.Display F] {I : C} {I' : C} {J : 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.Display.castToHom w' Y) = CategoryTheory.Display.cast ⋯ (CategoryTheory.DisplayStruct.comp_over (CategoryTheory.Display.castToHom w X) (CategoryTheory.Display.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.

@[simp]

theorem CategoryTheory.Display.castEquiv_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [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.Display.castEquiv w) g = w ▸ g

@[simp]

theorem CategoryTheory.Display.castEquiv_symm_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [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.Display.castEquiv w).symm g = ⋯ ▸ g

def CategoryTheory.Display.castEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [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.Display.castEquiv w = { toFun := fun (g : X ⟶[f] Y) => w ▸ g, invFun := fun (g : X ⟶[f'] Y) => ⋯ ▸ g, left_inv := ⋯, right_inv := ⋯ }

def CategoryTheory.Display.Total {C : Type u₁} (F : C → Type u₂) : Type (max u₁ u₂)

The total space of a displayed category consists of pairs (I, X) where I is an object of C and X is an object of the Fiber F I.

Equations

• ∫ F = ((I : C) × F I)

def CategoryTheory.Display.«term∫_» : Lean.ParserDescr

Equations

• CategoryTheory.Display.«term∫_» = Lean.ParserDescr.node `CategoryTheory.Display.term∫_ 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∫ ") (Lean.ParserDescr.cat `term 75))

def CategoryTheory.Display.Total.mk {C : Type u₁} {F : C → Type u₂} {I : C} (X : F I) : ∫ F

Equations

• CategoryTheory.Display.Total.mk X = ⟨I, X⟩

@[reducible, inline]

abbrev CategoryTheory.Display.Total.Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [CategoryTheory.Display F] (X : ∫ F) (Y : ∫ F) : Type (max v₁ u_1)

Equations

• X.Hom Y = ((f : X.fst ⟶ Y.fst) × X.snd ⟶[f] Y.snd)

@[simp]

theorem CategoryTheory.Display.Total.Hom.mk_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [CategoryTheory.Display F] {I : C} {J : C} {X : F I} {Y : F J} {f : I ⟶ J} (g : X ⟶[f] Y) : (CategoryTheory.Display.Total.Hom.mk g).snd = g

@[simp]

theorem CategoryTheory.Display.Total.Hom.mk_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [CategoryTheory.Display F] {I : C} {J : C} {X : F I} {Y : F J} {f : I ⟶ J} (g : X ⟶[f] Y) : (CategoryTheory.Display.Total.Hom.mk g).fst = f

def CategoryTheory.Display.Total.Hom.mk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [CategoryTheory.Display F] {I : C} {J : C} {X : F I} {Y : F J} {f : I ⟶ J} (g : X ⟶[f] Y) : (CategoryTheory.Display.Total.mk X).Hom (CategoryTheory.Display.Total.mk Y)

Equations

• CategoryTheory.Display.Total.Hom.mk g = ⟨f, g⟩

instance CategoryTheory.Display.Total.categoryStruct {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [CategoryTheory.Display F] : CategoryTheory.CategoryStruct.{max u_1 v₁, max u₂ u₁} ( ∫ F)

Equations

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

@[simp]

theorem CategoryTheory.Display.Total.cast_exchange_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [CategoryTheory.Display F] {I : C} {J : C} {K : C} {f : I ⟶ J} {f' : I ⟶ J} {h : J ⟶ K} {h' : J ⟶ K} {X : F I} {Y : F J} {Z : F K} (g : X ⟶[f] Y) (k : Y ⟶[h] Z) (w : f = f') (w' : h = h') : w' ▸ CategoryTheory.DisplayStruct.comp_over g k = CategoryTheory.DisplayStruct.comp_over (⋯ ▸ ⋯ ▸ g) (w' ▸ k)

@[simp]

theorem CategoryTheory.Display.Total.whisker_left_cast_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [CategoryTheory.Display F] {I : C} {J : C} {K : C} {f : I ⟶ J} {h : J ⟶ K} {h' : J ⟶ K} {X : F I} {Y : F J} {Z : F K} (g : X ⟶[f] Y) (k : Y ⟶[h] Z) (w : h = h') : ⋯ ▸ CategoryTheory.DisplayStruct.comp_over g k = CategoryTheory.DisplayStruct.comp_over g (w ▸ k)

@[simp]

theorem CategoryTheory.Display.Total.whisker_right_cast_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [CategoryTheory.Display F] {I : C} {J : C} {K : C} {f : I ⟶ J} {f' : I ⟶ J} {h : J ⟶ K} {X : F I} {Y : F J} {Z : F K} (g : X ⟶[f] Y) (k : Y ⟶[h] Z) (w : f = f') : ⋯ ▸ CategoryTheory.DisplayStruct.comp_over g k = CategoryTheory.DisplayStruct.comp_over (w ▸ g) k

instance CategoryTheory.Display.Total.category {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [CategoryTheory.Display F] : CategoryTheory.Category.{max v₁ u_1, max u₂ u₁} ( ∫ F)

Equations

• CategoryTheory.Display.Total.category = CategoryTheory.Category.mk ⋯ ⋯ ⋯

structure CategoryTheory.BasedLift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {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.

• hom : ↑X ⟶ ↑Y
• over_eq : CategoryTheory.CategoryStruct.comp (P.map self.hom) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f

theorem CategoryTheory.BasedLift.over_eq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {f : I ⟶ J} {X : P ⁻¹ I} {Y : P ⁻¹ J} (self : CategoryTheory.BasedLift f X Y) : CategoryTheory.CategoryStruct.comp (P.map self.hom) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f

def CategoryTheory.BasedLift' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {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.

structure CategoryTheory.EBasedLift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {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       ≅

• hom : X.obj ⟶ Y.obj
• over_eq : CategoryTheory.CategoryStruct.comp (P.map self.hom) Y.iso.hom = CategoryTheory.CategoryStruct.comp X.iso.hom f

theorem CategoryTheory.EBasedLift.over_eq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {f : I ⟶ J} {X : P ⁻¹ᵉ I} {Y : P ⁻¹ᵉ J} (self : CategoryTheory.EBasedLift f X Y) : CategoryTheory.CategoryStruct.comp (P.map self.hom) Y.iso.hom = CategoryTheory.CategoryStruct.comp X.iso.hom f

theorem CategoryTheory.EBasedLift.over_eq_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {f : I ⟶ J} {X : P ⁻¹ᵉ I} {Y : P ⁻¹ᵉ J} (self : CategoryTheory.EBasedLift f X Y) {Z : C} (h : J ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.map self.hom) (CategoryTheory.CategoryStruct.comp Y.iso.hom h) = CategoryTheory.CategoryStruct.comp X.iso.hom (CategoryTheory.CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.BasedLift.over_eq' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_2} [CategoryTheory.Category.{u_3, u_2} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {f : I ⟶ J} {X : P ⁻¹ I} {Y : P ⁻¹ J} (g : CategoryTheory.BasedLift f X Y) : P.map g.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))

@[simp]

theorem CategoryTheory.BasedLift.id_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_2} [CategoryTheory.Category.{u_3, u_2} E] {P : CategoryTheory.Functor E C} {I : C} (X : P ⁻¹ I) : (CategoryTheory.BasedLift.id X).hom = CategoryTheory.CategoryStruct.id ↑X

def CategoryTheory.BasedLift.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_2} [CategoryTheory.Category.{u_3, u_2} E] {P : CategoryTheory.Functor E C} {I : C} (X : P ⁻¹ I) : CategoryTheory.BasedLift (CategoryTheory.CategoryStruct.id I) X X

The identity based-lift.

Equations

• CategoryTheory.BasedLift.id X = { hom := CategoryTheory.CategoryStruct.id ↑X, over_eq := ⋯ }

@[simp]

theorem CategoryTheory.BasedLift.comp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_2} [CategoryTheory.Category.{u_3, u_2} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {K : C} {f₁ : I ⟶ J} {f₂ : J ⟶ K} {X : P ⁻¹ I} {Y : P ⁻¹ J} {Z : P ⁻¹ K} (g₁ : CategoryTheory.BasedLift f₁ X Y) (g₂ : CategoryTheory.BasedLift f₂ Y Z) : (g₁.comp g₂).hom = CategoryTheory.CategoryStruct.comp g₁.hom g₂.hom

def CategoryTheory.BasedLift.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_2} [CategoryTheory.Category.{u_3, u_2} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {K : C} {f₁ : I ⟶ J} {f₂ : J ⟶ K} {X : P ⁻¹ I} {Y : P ⁻¹ J} {Z : P ⁻¹ K} (g₁ : CategoryTheory.BasedLift f₁ X Y) (g₂ : CategoryTheory.BasedLift f₂ Y Z) : CategoryTheory.BasedLift (CategoryTheory.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 := ⋯ }

@[simp]

theorem CategoryTheory.BasedLift.cast_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_2} [CategoryTheory.Category.{u_3, u_2} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : P ⁻¹ I} {Y : P ⁻¹ J} (w : f = f') (g : CategoryTheory.BasedLift f X Y) : (CategoryTheory.BasedLift.cast w g).hom = g.hom

def CategoryTheory.BasedLift.cast {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_2} [CategoryTheory.Category.{u_3, u_2} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : P ⁻¹ I} {Y : P ⁻¹ J} (w : f = f') (g : CategoryTheory.BasedLift f X Y) : CategoryTheory.BasedLift f' X Y

Equations

• CategoryTheory.BasedLift.cast w g = { hom := g.hom, over_eq := ⋯ }

@[simp]

theorem CategoryTheory.EBasedLift.over_eq' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {f : I ⟶ J} {X : P ⁻¹ᵉ I} {Y : P ⁻¹ᵉ J} (g : CategoryTheory.EBasedLift f X Y) : P.map g.hom = CategoryTheory.CategoryStruct.comp X.iso.hom (CategoryTheory.CategoryStruct.comp f Y.iso.inv)

@[simp]

theorem CategoryTheory.EBasedLift.id_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} (X : P ⁻¹ᵉ I) : (CategoryTheory.EBasedLift.id X).hom = CategoryTheory.CategoryStruct.id X.obj

def CategoryTheory.EBasedLift.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} (X : P ⁻¹ᵉ I) : CategoryTheory.EBasedLift (CategoryTheory.CategoryStruct.id I) X X

Equations

• CategoryTheory.EBasedLift.id X = { hom := CategoryTheory.CategoryStruct.id X.obj, over_eq := ⋯ }

@[simp]

theorem CategoryTheory.EBasedLift.comp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {K : C} {f₁ : I ⟶ J} {f₂ : J ⟶ K} {X : P ⁻¹ᵉ I} {Y : P ⁻¹ᵉ J} {Z : P ⁻¹ᵉ K} (g₁ : CategoryTheory.EBasedLift f₁ X Y) (g₂ : CategoryTheory.EBasedLift f₂ Y Z) : (g₁.comp g₂).hom = CategoryTheory.CategoryStruct.comp g₁.hom g₂.hom

def CategoryTheory.EBasedLift.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {K : C} {f₁ : I ⟶ J} {f₂ : J ⟶ K} {X : P ⁻¹ᵉ I} {Y : P ⁻¹ᵉ J} {Z : P ⁻¹ᵉ K} (g₁ : CategoryTheory.EBasedLift f₁ X Y) (g₂ : CategoryTheory.EBasedLift f₂ Y Z) : CategoryTheory.EBasedLift (CategoryTheory.CategoryStruct.comp f₁ f₂) X Z

Equations

• g₁.comp g₂ = { hom := CategoryTheory.CategoryStruct.comp g₁.hom g₂.hom, over_eq := ⋯ }

@[simp]

theorem CategoryTheory.EBasedLift.cast_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : P ⁻¹ᵉ I} {Y : P ⁻¹ᵉ J} (w : f = f') (g : CategoryTheory.EBasedLift f X Y) : (CategoryTheory.EBasedLift.cast w g).hom = g.hom

def CategoryTheory.EBasedLift.cast {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : P ⁻¹ᵉ I} {Y : P ⁻¹ᵉ J} (w : f = f') (g : CategoryTheory.EBasedLift f X Y) : CategoryTheory.EBasedLift f' X Y

Equations

• CategoryTheory.EBasedLift.cast w g = { hom := g.hom, over_eq := ⋯ }

instance CategoryTheory.Functor.displayStruct {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] (P : CategoryTheory.Functor E C) : CategoryTheory.DisplayStruct fun (I : C) => P ⁻¹ I

The display structure DisplayStruct 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₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] (P : CategoryTheory.Functor E C) : CategoryTheory.DisplayStruct fun (I : C) => P ⁻¹ᵉ I

Equations

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

theorem CategoryTheory.BasedLift.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {f : I ⟶ J} {X : P ⁻¹ I} {Y : P ⁻¹ J} (g : X ⟶[f] Y) (g' : X ⟶[f] Y) (w : g.hom = g'.hom) : g = g'

@[simp]

theorem CategoryTheory.BasedLift.cast_rec {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : P ⁻¹ I} {Y : P ⁻¹ J} {w : f = f'} (g : X ⟶[f] Y) : CategoryTheory.BasedLift.cast w g = w ▸ g

@[simp]

theorem CategoryTheory.BasedLift.tauto_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {X : E} {Y : E} (g : X ⟶ Y) : (CategoryTheory.BasedLift.tauto g).hom = g

def CategoryTheory.BasedLift.tauto {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {X : E} {Y : E} (g : X ⟶ Y) : CategoryTheory.Fiber.tauto X ⟶[P.map g] CategoryTheory.Fiber.tauto 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 := ⋯ }

theorem CategoryTheory.BasedLift.tauto_over_base {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {X : E} {Y : E} (f : P.obj X ⟶ P.obj Y) (g : CategoryTheory.Fiber.tauto X ⟶[f] CategoryTheory.Fiber.tauto Y) : P.map g.hom = f

theorem CategoryTheory.BasedLift.tauto_comp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {X : E} {Y : E} {Z : E} {g : X ⟶ Y} {g' : Y ⟶ Z} : (CategoryTheory.DisplayStruct.comp_over (CategoryTheory.BasedLift.tauto g) (CategoryTheory.BasedLift.tauto g')).hom = CategoryTheory.CategoryStruct.comp g g'

theorem CategoryTheory.BasedLift.comp_tauto_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {X : E} {Y : E} {Z : E} {f : P.obj X ⟶ P.obj Y} {f' : CategoryTheory.Fiber.tauto X ⟶[f] CategoryTheory.Fiber.tauto Y} {g : Y ⟶ Z} : (CategoryTheory.DisplayStruct.comp_over f' (CategoryTheory.BasedLift.tauto g)).hom = CategoryTheory.CategoryStruct.comp f'.hom g

@[simp]

theorem CategoryTheory.BasedLift.instCoeTautoBasedLift_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {X : E} {Y : E} {g : X ⟶ Y} : CoeDep.coe g = CategoryTheory.BasedLift.tauto g

instance CategoryTheory.BasedLift.instCoeTautoBasedLift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {X : E} {Y : E} {g : X ⟶ Y} : CoeDep (X ⟶ Y) g (CategoryTheory.Fiber.tauto X ⟶[P.map g] CategoryTheory.Fiber.tauto Y)

A morphism of E coerced as a tautological based-lift.

Equations

• CategoryTheory.BasedLift.instCoeTautoBasedLift = { coe := CategoryTheory.BasedLift.tauto g }

theorem CategoryTheory.BasedLift.eq_id_of_hom_eq_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {X : P ⁻¹ I} {g : X ⟶[CategoryTheory.CategoryStruct.id I] X} : g.hom = CategoryTheory.CategoryStruct.id ↑X ↔ g = CategoryTheory.BasedLift.id X

@[simp]

theorem CategoryTheory.BasedLift.id_comp_cast {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {f : I ⟶ J} {X : P ⁻¹ I} {Y : P ⁻¹ J} {g : X ⟶[f] Y} : CategoryTheory.DisplayStruct.comp_over (𝟙ₒ X) g = CategoryTheory.BasedLift.cast ⋯ g

@[simp]

theorem CategoryTheory.BasedLift.comp_id_cast {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {f : I ⟶ J} {X : P ⁻¹ I} {Y : P ⁻¹ J} {g : X ⟶[f] Y} : CategoryTheory.DisplayStruct.comp_over g (𝟙ₒ Y) = CategoryTheory.BasedLift.cast ⋯ g

@[simp]

theorem CategoryTheory.BasedLift.assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {K : C} {L : C} {f : I ⟶ J} {h : J ⟶ K} {l : K ⟶ L} {W : P ⁻¹ I} {X : P ⁻¹ J} {Y : P ⁻¹ K} {Z : P ⁻¹ L} (g : W ⟶[f] X) (k : X ⟶[h] Y) (m : Y ⟶[l] Z) : CategoryTheory.DisplayStruct.comp_over (CategoryTheory.DisplayStruct.comp_over g k) m = CategoryTheory.BasedLift.cast ⋯ (CategoryTheory.DisplayStruct.comp_over g (CategoryTheory.DisplayStruct.comp_over k m))

def CategoryTheory.BasedLift.eqToHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {X : P ⁻¹ I} {Y : P ⁻¹ I} (w : X = Y) : X ⟶[CategoryTheory.CategoryStruct.id I] Y

Equations

• CategoryTheory.BasedLift.eqToHom w = w ▸ CategoryTheory.BasedLift.id X

def CategoryTheory.BasedLift.eqToHom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {X : P ⁻¹ I} {Y : P ⁻¹ I} (w : ↑X = ↑Y) : X ⟶[CategoryTheory.CategoryStruct.id I] Y

Equations

• CategoryTheory.BasedLift.eqToHom' w = ⋯ ▸ CategoryTheory.BasedLift.id X

theorem CategoryTheory.EBasedLift.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] (P : CategoryTheory.Functor E C) {I : C} {J : C} {f : I ⟶ J} {X : P ⁻¹ᵉ I} {Y : P ⁻¹ᵉ J} (g : X ⟶[f] Y) (g' : X ⟶[f] Y) (w : g.hom = g'.hom) : g = g'

@[simp]

theorem CategoryTheory.EBasedLift.cast_rec {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] (P : CategoryTheory.Functor E C) {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : P ⁻¹ᵉ I} {Y : P ⁻¹ᵉ J} {w : f = f'} (g : X ⟶[f] Y) : CategoryTheory.EBasedLift.cast w g = w ▸ g

@[simp]

theorem CategoryTheory.EBasedLift.tauto_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {X : E} {Y : E} (g : X ⟶ Y) : (CategoryTheory.EBasedLift.tauto g).hom = g

def CategoryTheory.EBasedLift.tauto {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {X : E} {Y : E} (g : X ⟶ Y) : CategoryTheory.EFiber.tauto X ⟶[P.map g] CategoryTheory.EFiber.tauto 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 := ⋯ }

theorem CategoryTheory.EBasedLift.tauto_over_base {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {X : E} {Y : E} (f : P.obj X ⟶ P.obj Y) (g : CategoryTheory.Fiber.tauto X ⟶[f] CategoryTheory.Fiber.tauto Y) : P.map g.hom = f

theorem CategoryTheory.EBasedLift.tauto_comp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {X : E} {Y : E} {Z : E} {g : X ⟶ Y} {g' : Y ⟶ Z} : (CategoryTheory.DisplayStruct.comp_over (CategoryTheory.EBasedLift.tauto g) (CategoryTheory.EBasedLift.tauto g')).hom = CategoryTheory.CategoryStruct.comp g g'

theorem CategoryTheory.EBasedLift.comp_tauto_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {X : E} {Y : E} {Z : E} {f : P.obj X ⟶ P.obj Y} {f' : CategoryTheory.EFiber.tauto X ⟶[f] CategoryTheory.EFiber.tauto Y} {g : Y ⟶ Z} : (CategoryTheory.DisplayStruct.comp_over f' (CategoryTheory.EBasedLift.tauto g)).hom = CategoryTheory.CategoryStruct.comp f'.hom g

@[simp]

theorem CategoryTheory.EBasedLift.instCoeTautoBasedLift_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {X : E} {Y : E} {g : X ⟶ Y} : CoeDep.coe g = CategoryTheory.EBasedLift.tauto g

instance CategoryTheory.EBasedLift.instCoeTautoBasedLift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {X : E} {Y : E} {g : X ⟶ Y} : CoeDep (X ⟶ Y) g (CategoryTheory.EFiber.tauto X ⟶[P.map g] CategoryTheory.EFiber.tauto Y)

A morphism of E coerced as a tautological based-lift.

Equations

• CategoryTheory.EBasedLift.instCoeTautoBasedLift = { coe := CategoryTheory.EBasedLift.tauto g }

theorem CategoryTheory.EBasedLift.eq_id_of_hom_eq_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {X : P ⁻¹ᵉ I} {g : X ⟶[CategoryTheory.CategoryStruct.id I] X} : g.hom = CategoryTheory.CategoryStruct.id X.obj ↔ g = CategoryTheory.EBasedLift.id X

@[simp]

theorem CategoryTheory.EBasedLift.id_comp_cast {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {f : I ⟶ J} {X : P ⁻¹ᵉ I} {Y : P ⁻¹ᵉ J} {g : X ⟶[f] Y} : CategoryTheory.DisplayStruct.comp_over (𝟙ₒ X) g = CategoryTheory.EBasedLift.cast ⋯ g

@[simp]

theorem CategoryTheory.EBasedLift.comp_id_cast {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {f : I ⟶ J} {X : P ⁻¹ᵉ I} {Y : P ⁻¹ᵉ J} {g : X ⟶[f] Y} : CategoryTheory.DisplayStruct.comp_over g (𝟙ₒ Y) = CategoryTheory.EBasedLift.cast ⋯ g

@[simp]

theorem CategoryTheory.EBasedLift.assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {K : C} {L : C} {f : I ⟶ J} {h : J ⟶ K} {l : K ⟶ L} {W : P ⁻¹ᵉ I} {X : P ⁻¹ᵉ J} {Y : P ⁻¹ᵉ K} {Z : P ⁻¹ᵉ L} (g : W ⟶[f] X) (k : X ⟶[h] Y) (m : Y ⟶[l] Z) : CategoryTheory.DisplayStruct.comp_over (CategoryTheory.DisplayStruct.comp_over g k) m = CategoryTheory.EBasedLift.cast ⋯ (CategoryTheory.DisplayStruct.comp_over g (CategoryTheory.DisplayStruct.comp_over k m))

instance CategoryTheory.Functor.display {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] (P : CategoryTheory.Functor E C) : CategoryTheory.Display fun (I : C) => P ⁻¹ I

The displayed category of a functor P : E ⥤ C.

Equations

• P.display = CategoryTheory.Display.mk ⋯ ⋯ ⋯

instance CategoryTheory.Functor.edisplay {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] (P : CategoryTheory.Functor E C) : CategoryTheory.Display fun (I : C) => P ⁻¹ᵉ I

Equations

• P.edisplay = CategoryTheory.Display.mk ⋯ ⋯ ⋯

structure CategoryTheory.Display.Lift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [CategoryTheory.Display F] {I : C} {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
• homOver : self.src ⟶[f] tgt

theorem CategoryTheory.Display.Lift.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {tgt : F J} {g : CategoryTheory.Display.Lift f tgt} {g' : CategoryTheory.Display.Lift f tgt} (w_src : g.src = g'.src) (w_homOver : g.homOver = ⋯ ▸ g'.homOver) : g = g'

theorem CategoryTheory.Display.CoLift.ext {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {F : C → Type u₂} {inst_1 : CategoryTheory.Display F} {I J : C} {f : I ⟶ J} {src : F I} (x y : CategoryTheory.Display.CoLift f src), x.tgt = y.tgt → HEq x.homOver y.homOver → x = y

theorem CategoryTheory.Display.CoLift.ext_iff {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {F : C → Type u₂} {inst_1 : CategoryTheory.Display F} {I J : C} {f : I ⟶ J} {src : F I} (x y : CategoryTheory.Display.CoLift f src), x = y ↔ x.tgt = y.tgt ∧ HEq x.homOver y.homOver

structure CategoryTheory.Display.CoLift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : C → Type u₂} [CategoryTheory.Display F] {I : C} {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
• homOver : src ⟶[f] self.tgt