class DisplayStruct {C : Type u} [CategoryTheory.Category.{u_1, u} C] {𝔼 : C} {𝕌 : C} (π : 𝔼 ⟶ 𝕌) {D : C} {A : C} (p : D ⟶ A) : Type u_1

• char : A ⟶ 𝕌
• var : D ⟶ 𝔼
• disp_pullback : CategoryTheory.IsPullback (DisplayStruct.var π p) p π (DisplayStruct.char π p)

theorem DisplayStruct.disp_pullback {C : Type u} [CategoryTheory.Category.{u_1, u} C] {𝔼 : C} {𝕌 : C} {π : 𝔼 ⟶ 𝕌} {D : C} {A : C} {p : D ⟶ A} [self : DisplayStruct π p] : CategoryTheory.IsPullback (DisplayStruct.var π p) p π (DisplayStruct.char π p)

def IsDisplay {C : Type u} [CategoryTheory.Category.{u_1, u} C] {𝔼 : C} {𝕌 : C} (π : 𝔼 ⟶ 𝕌) : CategoryTheory.MorphismProperty C

Equations

• IsDisplay π p = Nonempty (DisplayStruct π p)

structure Disp' {C : Type u} [CategoryTheory.Category.{u_1, u} C] {𝔼 : C} {𝕌 : C} (π : 𝔼 ⟶ 𝕌) : Type (max u u_1)

• T : C
• B : C
• p : self.T ⟶ self.B
• disp : DisplayStruct π self.p

@[reducible, inline]

abbrev Cart (C : Type u) [CategoryTheory.Category.{u_1, u} C] : Type (max u u_1)

Cart C is a typeclass synonym for Arrow C which comes equipped with a cateogry structure whereby morphisms between arrows p and q are cartesian squares between them.

Equations

• Cart C = CategoryTheory.Arrow C

@[simp]

theorem IsPullback.of_horiz_id {C : Type u} [CategoryTheory.Category.{u_1, u} C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.id X) f f (CategoryTheory.CategoryStruct.id Y)

instance instCategoryCart {C : Type u} [CategoryTheory.Category.{u_1, u} C] : CategoryTheory.Category.{u_1, max u_1 u} (Cart C)

Equations

• instCategoryCart = CategoryTheory.Category.mk ⋯ ⋯ ⋯

def WideSubcategory (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : Type (max u_1 u_2)

Equations

• WideSubcategory C = WideSubquiver C

def displayStructPresheaf {C : Type u} [CategoryTheory.Category.{u, u} C] {𝔼 : C} {𝕌 : C} (π : 𝔼 ⟶ 𝕌) : CategoryTheory.Functor (Cart C)ᵒᵖ (Type u)

Equations

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

@[reducible, inline]

abbrev Disp {C : Type u} [CategoryTheory.Category.{u, u} C] {𝔼 : C} {𝕌 : C} (π : 𝔼 ⟶ 𝕌) : Type u

Equations

• Disp π = (displayStructPresheaf π).Elementsᵒᵖ

def forget {C : Type u} [CategoryTheory.Category.{u, u} C] {𝔼 : C} {𝕌 : C} (π : 𝔼 ⟶ 𝕌) : CategoryTheory.Functor (Disp π) (Cart C)

Equations

• forget π = (CategoryTheory.CategoryOfElements.π (displayStructPresheaf π)).leftOp

structure DisplayStruct.Hom {C : Type u} [CategoryTheory.Category.{u_1, u} C] {𝔼 : C} {𝕌 : C} (π : 𝔼 ⟶ 𝕌) {D : C} {A : C} {E : C} {B : C} (p : D ⟶ A) [i : DisplayStruct π p] (q : E ⟶ B) [j : DisplayStruct π q] : Type u_1

• base : B ⟶ A
• base_eq : CategoryTheory.CategoryStruct.comp self.base (DisplayStruct.char π p) = DisplayStruct.char π q

theorem DisplayStruct.Hom.base_eq {C : Type u} [CategoryTheory.Category.{u_1, u} C] {𝔼 : C} {𝕌 : C} {π : 𝔼 ⟶ 𝕌} {D : C} {A : C} {E : C} {B : C} {p : D ⟶ A} [i : DisplayStruct π p] {q : E ⟶ B} [j : DisplayStruct π q] (self : DisplayStruct.Hom π p q) : CategoryTheory.CategoryStruct.comp self.base (DisplayStruct.char π p) = DisplayStruct.char π q

instance DisplayStruct.category {C : Type u} [CategoryTheory.Category.{u_1, u} C] {𝔼 : C} {𝕌 : C} (π : 𝔼 ⟶ 𝕌) : CategoryTheory.Category.{u_1, max u_1 u} (Disp' π)

Equations

• DisplayStruct.category π = CategoryTheory.Category.mk ⋯ ⋯ ⋯

theorem DisplayStruct.is_cartesian {C : Type u} [CategoryTheory.Category.{u_1, u} C] {𝔼 : C} {𝕌 : C} (π : 𝔼 ⟶ 𝕌) {Q : Disp' π} {P : Disp' π} (f : Q ⟶ P) : let cone := CategoryTheory.Limits.PullbackCone.mk (DisplayStruct.var π Q.p) (CategoryTheory.CategoryStruct.comp Q.p ↑f) ⋯; CategoryTheory.IsPullback (⋯.isLimit.lift cone) Q.p P.p ↑f

A morphism of display maps is necessarily cartesian: The cartesian square is obtained by the pullback pasting lemma.

def DisplayStruct.pullback {C : Type u} [CategoryTheory.Category.{u_1, u} C] {D : C} {A : C} {E : C} {B : C} (π : E ⟶ B) (p : D ⟶ A) (q : E ⟶ B) [i : DisplayStruct π p] [j : DisplayStruct π q] (t : B ⟶ A) (h : CategoryTheory.CategoryStruct.comp t (DisplayStruct.char π p) = DisplayStruct.char π q) : DisplayStruct p q

Equations

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

def DisplayStruct.displayMapOfPullback {C : Type u} [CategoryTheory.Category.{u_1, u} C] [CategoryTheory.Limits.HasPullbacks C] {𝔼 : C} {𝕌 : C} (π : 𝔼 ⟶ 𝕌) {D : C} {A : C} {B : C} (p : D ⟶ A) [i : DisplayStruct π p] (t : B ⟶ A) : DisplayStruct π CategoryTheory.Limits.pullback.snd

Equations

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

instance instDisplayStructPshTpMapFunctorOppositeTypeYonedaDisp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.NaturalModel.NaturalModelBase Ctx] (Γ : Ctx) (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Ty) : DisplayStruct CategoryTheory.NaturalModel.tp (CategoryTheory.yoneda.map (CategoryTheory.NaturalModel.disp Γ A))

Equations

• instDisplayStructPshTpMapFunctorOppositeTypeYonedaDisp Γ A = { char := A, var := CategoryTheory.NaturalModel.var Γ A, disp_pullback := ⋯ }