Locally cartesian closed categories

class LCC (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] : Type (max u v)

• over_cc : (I : C) → CategoryTheory.CartesianClosed (CategoryTheory.Over I)
• pushforward : {X Y : C} → (X ⟶ Y) → CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.Over Y)
• adj : {X Y : C} → autoParam ((f : X ⟶ Y) → Δ_ f ⊣ LCC.pushforward f) _auto✝

class OverCC (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] : Type (max u v)

• over_cc : (I : C) → CategoryTheory.CartesianClosed (CategoryTheory.Over I)

class PushforwardAdj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] : Type (max u v)

• pushforward : {X Y : C} → (X ⟶ Y) → CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.Over Y)
• adj : {X Y : C} → autoParam ((f : X ⟶ Y) → Δ_ f ⊣ PushforwardAdj.pushforward f) _auto✝

def OverBinaryProduct.pullbackCompositionIsBinaryProduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} (f : CategoryTheory.Over I) (x : CategoryTheory.Over I) : let pbleg1 := CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.snd x.hom f.hom) ⋯; let pbleg2 := CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.fst x.hom f.hom) ⋯; CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk pbleg1 pbleg2)

Equations

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

def OverBinaryProduct.OverProdIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] {I : C} (f : CategoryTheory.Over I) (x : CategoryTheory.Over I) : (Σ_ f.hom).obj ((Δ_ f.hom).obj x) ≅ f ⨯ x

Equations

• OverBinaryProduct.OverProdIso f x = CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso (OverBinaryProduct.pullbackCompositionIsBinaryProduct f x) (CategoryTheory.Limits.prodIsProd f x)

def OverBinaryProduct.OverProdIso.symm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] {I : C} (f : CategoryTheory.Over I) (x : CategoryTheory.Over I) : f ⨯ x ≅ (Σ_ f.hom).obj ((Δ_ f.hom).obj x)

Equations

• OverBinaryProduct.OverProdIso.symm f x = (CategoryTheory.Limits.prodIsProd f x).conePointUniqueUpToIso (OverBinaryProduct.pullbackCompositionIsBinaryProduct f x)

@[simp]

theorem OverBinaryProduct.OverProdIsoLeftInv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] {I : C} (f : CategoryTheory.Over I) (x : CategoryTheory.Over I) : CategoryTheory.CategoryStruct.comp (OverBinaryProduct.OverProdIso f x).hom (OverBinaryProduct.OverProdIso.symm f x).hom = CategoryTheory.CategoryStruct.id ((Σ_ f.hom).obj ((Δ_ f.hom).obj x))

@[simp]

theorem OverBinaryProduct.OverProdIsoRightInv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] {I : C} (f : CategoryTheory.Over I) (x : CategoryTheory.Over I) : CategoryTheory.CategoryStruct.comp (OverBinaryProduct.OverProdIso.symm f x).hom (OverBinaryProduct.OverProdIso f x).hom = CategoryTheory.CategoryStruct.id (f ⨯ x)

@[simp]

theorem OverBinaryProduct.Triangle_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] {I : C} (f : CategoryTheory.Over I) (x : CategoryTheory.Over I) : let pbleg1 := CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.snd x.hom f.hom) ⋯; CategoryTheory.CategoryStruct.comp (OverBinaryProduct.OverProdIso f x).hom CategoryTheory.Limits.prod.fst = pbleg1

@[simp]

theorem OverBinaryProduct.Triangle_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] {I : C} (f : CategoryTheory.Over I) (x : CategoryTheory.Over I) : let pbleg2 := CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.fst x.hom f.hom) ⋯; CategoryTheory.CategoryStruct.comp (OverBinaryProduct.OverProdIso f x).hom CategoryTheory.Limits.prod.snd = pbleg2

@[simp]

theorem OverBinaryProduct.Triangle.symm_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] {I : C} (f : CategoryTheory.Over I) (x : CategoryTheory.Over I) : let pbleg1 := CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.snd x.hom f.hom) ⋯; CategoryTheory.CategoryStruct.comp (OverBinaryProduct.OverProdIso.symm f x).hom pbleg1 = CategoryTheory.Limits.prod.fst

@[simp]

theorem OverBinaryProduct.Triangle.symm_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] {I : C} (f : CategoryTheory.Over I) (x : CategoryTheory.Over I) : let pbleg2 := CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.fst x.hom f.hom) ⋯; CategoryTheory.CategoryStruct.comp (OverBinaryProduct.OverProdIso.symm f x).hom pbleg2 = CategoryTheory.Limits.prod.snd

def OverBinaryProduct.NatOverProdIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] {I : C} (f : CategoryTheory.Over I) : (Δ_ f.hom).comp (Σ_ f.hom) ≅ CategoryTheory.MonoidalCategory.tensorLeft f

Equations

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

instance PushforwardAdj.cartesianClosedOfOver {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [PushforwardAdj C] {I : C} : CategoryTheory.CartesianClosed (CategoryTheory.Over I)

Equations

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

instance PushforwardAdj.instOverCC {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [PushforwardAdj C] : OverCC C

Equations

• PushforwardAdj.instOverCC = { over_cc := fun (I : C) => inferInstance }

def OverCC.pushforwardCospanLeg1 {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [OverCC C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id Y) ⟶ CategoryTheory.Over.mk f ⟹ CategoryTheory.Over.mk f

Equations

• OverCC.pushforwardCospanLeg1 f = CategoryTheory.CartesianClosed.curry CategoryTheory.Limits.prod.fst

def OverCC.pushforwardCospanLeg2 {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [OverCC C] {X : C} {Y : C} (f : X ⟶ Y) (x : CategoryTheory.Over X) : CategoryTheory.Over.mk f ⟹ (Σ_ f).obj x ⟶ CategoryTheory.Over.mk f ⟹ CategoryTheory.Over.mk f

Equations

• OverCC.pushforwardCospanLeg2 f x = (CategoryTheory.exp (CategoryTheory.Over.mk f)).map (CategoryTheory.Over.homMk x.hom ⋯)

def OverCC.pushforwardObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [OverCC C] {X : C} {Y : C} (f : X ⟶ Y) (x : CategoryTheory.Over X) : CategoryTheory.Over Y

Equations

• OverCC.pushforwardObj f x = CategoryTheory.Limits.pullback (OverCC.pushforwardCospanLeg1 f) (OverCC.pushforwardCospanLeg2 f x)

def OverCC.pushforwardCospanLeg2Map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [OverCC C] {X : C} {Y : C} (f : X ⟶ Y) (x : CategoryTheory.Over X) (x' : CategoryTheory.Over X) (u : x ⟶ x') : CategoryTheory.Over.mk f ⟹ (Σ_ f).obj x ⟶ CategoryTheory.Over.mk f ⟹ (Σ_ f).obj x'

Equations

• OverCC.pushforwardCospanLeg2Map f x x' u = (CategoryTheory.exp (CategoryTheory.Over.mk f)).map ((Σ_ f).map u)

def OverCC.pushforwardMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [OverCC C] {X : C} {Y : C} (f : X ⟶ Y) (x : CategoryTheory.Over X) (x' : CategoryTheory.Over X) (u : x ⟶ x') : OverCC.pushforwardObj f x ⟶ OverCC.pushforwardObj f x'

Equations

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

def OverCC.pushforwardFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [OverCC C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.Over Y)

Equations

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

def OverCC.PushforwardObjToLeg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [OverCC C] {X : C} {Y : C} (f : X ⟶ Y) (x : CategoryTheory.Over X) (y : CategoryTheory.Over Y) (u : (Δ_ f).obj y ⟶ x) : y ⟶ CategoryTheory.Over.mk f ⟹ (Σ_ f).obj x

Equations

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

def OverCC.PushforwardObjTo {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [OverCC C] {X : C} {Y : C} (f : X ⟶ Y) (x : CategoryTheory.Over X) (y : CategoryTheory.Over Y) (u : (Δ_ f).obj y ⟶ x) : y ⟶ (OverCC.pushforwardFunctor f).obj x

Equations

• OverCC.PushforwardObjTo f x y u = CategoryTheory.Limits.pullback.lift (CategoryTheory.Over.mkIdTerminal.from y) (OverCC.PushforwardObjToLeg f x y u) ⋯

def OverCC.PushforwardObjUP {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [OverCC C] {X : C} {Y : C} (f : X ⟶ Y) (x : CategoryTheory.Over X) (y : CategoryTheory.Over Y) (v : y ⟶ CategoryTheory.Over.mk f ⟹ (Σ_ f).obj x) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.mkIdTerminal.from y) (OverCC.pushforwardCospanLeg1 f) = CategoryTheory.CategoryStruct.comp v (OverCC.pushforwardCospanLeg2 f x)) : (Δ_ f).obj y ⟶ x

Equations

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

def OverCC.pushforwardAdjRightInv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [OverCC C] {X : C} {Y : C} (f : X ⟶ Y) (x : CategoryTheory.Over X) (y : CategoryTheory.Over Y) (v : y ⟶ CategoryTheory.Over.mk f ⟹ (Σ_ f).obj x) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.mkIdTerminal.from y) (OverCC.pushforwardCospanLeg1 f) = CategoryTheory.CategoryStruct.comp v (OverCC.pushforwardCospanLeg2 f x)) : OverCC.PushforwardObjToLeg f x y (OverCC.PushforwardObjUP f x y v w) = v

Equations

• ⋯ = ⋯

def OverCC.pushforwardAdj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [OverCC C] {X : C} {Y : C} (f : X ⟶ Y) : Δ_ f ⊣ OverCC.pushforwardFunctor f

Equations

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

instance OverCC.instPushforwardAdj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [OverCC C] : PushforwardAdj C

Equations

• OverCC.instPushforwardAdj = { pushforward := fun {X Y : C} (f : X ⟶ Y) => OverCC.pushforwardFunctor f, adj := fun {X Y : C} (f : X ⟶ Y) => OverCC.pushforwardAdj f }

def PushforwardAdj.idPullbackIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] (X : C) : CategoryTheory.Functor.id (CategoryTheory.Over X) ≅ Δ_ CategoryTheory.CategoryStruct.id X

Equations

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

def PushforwardAdj.idIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [PushforwardAdj C] (X : C) : PushforwardAdj.pushforward (CategoryTheory.CategoryStruct.id X) ≅ CategoryTheory.Functor.id (CategoryTheory.Over X)

Equations

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

instance LCCC.mkOfOverCC {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [OverCC C] : LCC C

Equations

• LCCC.mkOfOverCC = { over_cc := OverCC.over_cc, pushforward := fun {X Y : C} => OverCC.pushforwardFunctor, adj := fun {X Y : C} => OverCC.pushforwardAdj }

instance LCCC.mkOfPushforwardAdj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [PushforwardAdj C] : LCC C

Equations

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

instance Limits.WidePullbackShapeIsConnected (J : Type) : CategoryTheory.IsConnected (CategoryTheory.Limits.WidePullbackShape J)

Equations

• ⋯ = ⋯

instance Over.OverFiniteWidePullbacks {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] (I : C) : CategoryTheory.Limits.HasFiniteWidePullbacks (CategoryTheory.Over I)

Equations

• ⋯ = ⋯

instance LCCC.FiniteWidePullbacksTerminal.FiniteLimits {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] : CategoryTheory.Limits.HasFiniteLimits C

Equations

• ⋯ = ⋯

instance LCCC.cartesianClosed {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [OverCC C] : CategoryTheory.CartesianClosed C

Equations

• LCCC.cartesianClosed = CategoryTheory.cartesianClosedOfEquiv CategoryTheory.equivOverTerminal.symm

instance LCCC.OverLCC {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [OverCC C] (I : C) : LCC (CategoryTheory.Over I)

Equations

• LCCC.OverLCC I = LCCC.mkOfOverCC