theorem CategoryTheory.Over.isCartesian_mapPullbackAdj_counit {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) : NatTrans.IsCartesian (mapPullbackAdj f).counit

@[reducible, inline]

abbrev CategoryTheory.Over.Reindex {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X : C} (Y Z : Over X) : Over Y.left

The reindexing of Z : Over X along Y : Over X, defined by pulling back Z along Y.hom : Y.left ⟶ X.

Equations

• Y.Reindex Z = (CategoryTheory.Over.pullback Y.hom).obj Z

theorem CategoryTheory.Over.Reindex.hom {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X : C} {Y Z : Over X} : (Y.Reindex Z).hom = Limits.pullback.snd Z.hom Y.hom

def CategoryTheory.Over.Reindex.symmetryObjIso {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X : C} (Y Z : Over X) : (Y.Reindex Z).left ≅ (Z.Reindex Y).left

Reindex is symmetric in its first and second arguments up to an isomorphism.

Equations

• CategoryTheory.Over.Reindex.symmetryObjIso Y Z = CategoryTheory.Limits.pullbackSymmetry Z.hom Y.hom

def CategoryTheory.Over.Reindex.sigmaSymmetryIso {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X : C} (Y Z : Over X) : Y.Sigma (Y.Reindex Z) ≅ Z.Sigma (Z.Reindex Y)

The reindexed sum of Z along Y is isomorphic to the reindexed sum of Y along Z in the category Over X.

Equations

• CategoryTheory.Over.Reindex.sigmaSymmetryIso Y Z = CategoryTheory.Over.isoMk (CategoryTheory.Limits.pullbackSymmetry Z.hom Y.hom) ⋯

@[simp]

theorem CategoryTheory.Over.Reindex.sigmaSymmetryIso_hom_left {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X : C} (Y Z : Over X) : (sigmaSymmetryIso Y Z).hom.left = (Limits.pullbackSymmetry Z.hom Y.hom).hom

@[simp]

theorem CategoryTheory.Over.Reindex.sigmaSymmetryIso_inv_left {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X : C} (Y Z : Over X) : (sigmaSymmetryIso Y Z).inv.left = (Limits.pullbackSymmetry Z.hom Y.hom).inv

theorem CategoryTheory.Over.Reindex.symmetry_hom {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X : C} {Y Z : Over X} : CategoryStruct.comp (Limits.pullback.snd Z.hom Y.hom) Y.hom = CategoryStruct.comp (Limits.pullbackSymmetry Z.hom Y.hom).hom (CategoryStruct.comp (Limits.pullback.snd Y.hom Z.hom) Z.hom)

def CategoryTheory.Over.Reindex.fstProj {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X : C} (Y Z : Over X) : Y.Sigma (Y.Reindex Z) ⟶ Y

The first projection out of the reindexed sigma object.

Equations

• CategoryTheory.Over.Reindex.fstProj Y Z = CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.snd Z.hom Y.hom) ⋯

theorem CategoryTheory.Over.Reindex.fstProj_sigma_fst {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X : C} (Y Z : Over X) : fstProj Y Z = Sigma.fst (Y.Reindex Z)

def CategoryTheory.Over.Reindex.sndProj {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X : C} (Y Z : Over X) : Y.Sigma (Y.Reindex Z) ⟶ Z

The second projection out of the reindexed sigma object.

Equations

• CategoryTheory.Over.Reindex.sndProj Y Z = CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.fst Z.hom Y.hom) ⋯

def CategoryTheory.Over.Reindex.termπ_ : Lean.ParserDescr

The notation for the first projection of the reindexed sigma object.

Equations

• CategoryTheory.Over.Reindex.termπ_ = Lean.ParserDescr.node `CategoryTheory.Over.Reindex.termπ_ 1024 (Lean.ParserDescr.symbol " π_ ")

def CategoryTheory.Over.Reindex.termμ_ : Lean.ParserDescr

The notation for the second projection of the reindexed sigma object.

Equations

• CategoryTheory.Over.Reindex.termμ_ = Lean.ParserDescr.node `CategoryTheory.Over.Reindex.termμ_ 1024 (Lean.ParserDescr.symbol " μ_ ")

theorem CategoryTheory.Over.Reindex.counit_app_pullback_fst {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X : C} {Y Z : Over X} : sndProj Y Z = (mapPullbackAdj Y.hom).counit.app Z

theorem CategoryTheory.Over.Reindex.counit_app_pullback_snd {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X : C} {Y Z : Over X} : fstProj Y Z = CategoryStruct.comp (sigmaSymmetryIso Y Z).hom ((mapPullbackAdj Z.hom).counit.app Y)

@[simp]

theorem CategoryTheory.Over.Reindex.counit_app_pullback_snd_eq_homMk {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X : C} {Y Z : Over X} : fstProj Y Z = homMk (Y.Reindex Z).hom ⋯

def CategoryTheory.Over.isBinaryProductSigmaReindex {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteWidePullbacks C] {X : C} (Y Z : Over X) : Limits.IsLimit (Limits.BinaryFan.mk (Reindex.fstProj Y Z) (Reindex.sndProj Y Z))

The binary fan provided by μ_ and π_ is a binary product in Over X.

Equations

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

def CategoryTheory.Over.sigmaReindexIsoProd {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteWidePullbacks C] {X : C} (Y Z : Over X) : Y.Sigma (Y.Reindex Z) ≅ Y ⨯ Z

The object (Sigma Y) (Reindex Y Z) is isomorphic to the binary product Y × Z in Over X.

Equations

• Y.sigmaReindexIsoProd Z = (Y.isBinaryProductSigmaReindex Z).conePointUniqueUpToIso (CategoryTheory.Limits.prodIsProd Y Z)

@[simp]

theorem CategoryTheory.Over.sigmaReindexIsoProd_hom_left {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteWidePullbacks C] {X : C} (Y Z : Over X) : (Y.sigmaReindexIsoProd Z).hom.left = (Limits.limit.lift (Limits.pair Y Z) (Limits.BinaryFan.mk (Reindex.fstProj Y Z) (Reindex.sndProj Y Z))).left

@[simp]

theorem CategoryTheory.Over.sigmaReindexIsoProd_inv_left {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteWidePullbacks C] {X : C} (Y Z : Over X) : (Y.sigmaReindexIsoProd Z).inv.left = Limits.pullback.lift Limits.prod.snd.left Limits.prod.fst.left ⋯

@[simp]

theorem CategoryTheory.Over.sigmaReindexIsoProd_hom_right {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteWidePullbacks C] {X : C} (Y Z : Over X) : (Y.sigmaReindexIsoProd Z).hom.right = CategoryStruct.id (Y.Sigma (Y.Reindex Z)).right

def CategoryTheory.Over.sigmaReindexIsoProdMk {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteWidePullbacks C] {X Y : C} (f : Y ⟶ X) (Z : Over X) : (map f).obj ((pullback f).obj Z) ≅ mk f ⨯ Z

Given a morphism f : X' ⟶ X and an object Y over X, the (map f).obj ((pullback f).obj Y) is isomorphic to the binary product of (Over.mk f) and Y.

Equations

• CategoryTheory.Over.sigmaReindexIsoProdMk f Z = (CategoryTheory.Over.mk f).sigmaReindexIsoProd Z

theorem CategoryTheory.Over.sigmaReindexIsoProd_hom_comp_fst {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteWidePullbacks C] {X : C} {Y Z : Over X} : CategoryStruct.comp (Y.sigmaReindexIsoProd Z).hom (CartesianMonoidalCategory.fst Y Z) = Reindex.fstProj Y Z

theorem CategoryTheory.Over.sigmaReindexIsoProd_hom_comp_snd {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteWidePullbacks C] {X : C} {Y Z : Over X} : CategoryStruct.comp (Y.sigmaReindexIsoProd Z).hom (CartesianMonoidalCategory.snd Y Z) = Reindex.sndProj Y Z

def CategoryTheory.Over.sigmaReindexNatIsoTensorLeft {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteWidePullbacks C] {X : C} (Y : Over X) : (pullback Y.hom).comp (map Y.hom) ≅ MonoidalCategory.tensorLeft Y

The pull-push composition (Over.pullback Y.hom) ⋙ (Over.map Y.hom) is naturally isomorphic to the left tensor product functor Y × _ in Over X

Equations

• Y.sigmaReindexNatIsoTensorLeft = CategoryTheory.NatIso.ofComponents (fun (Z : CategoryTheory.Over ((CategoryTheory.Functor.fromPUnit X).obj Y.right)) => id (Y.sigmaReindexIsoProd Z)) ⋯

theorem CategoryTheory.Over.sigmaReindexNatIsoTensorLeft_hom_app {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteWidePullbacks C] {X : C} {Y : Over X} (Z : Over X) : Y.sigmaReindexNatIsoTensorLeft.hom.app Z = (Y.sigmaReindexIsoProd Z).hom

def CategoryTheory.Functor.toOverTerminal (C : Type u₁) [Category.{v₁, u₁} C] [Limits.HasTerminal C] : Functor C (Over (⊤_ C))

The functor from C to Over (⊤_ C) which sends X : C to terminal.from X.

Equations

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

@[simp]

theorem CategoryTheory.Functor.toOverTerminal_obj_hom (C : Type u₁) [Category.{v₁, u₁} C] [Limits.HasTerminal C] (X : C) : ((toOverTerminal C).obj X).hom = Limits.terminal.from X

@[simp]

theorem CategoryTheory.Functor.toOverTerminal_map_left (C : Type u₁) [Category.{v₁, u₁} C] [Limits.HasTerminal C] {X Y : C} (f : X ⟶ Y) : ((toOverTerminal C).map f).left = f

@[simp]

theorem CategoryTheory.Functor.toOverTerminal_obj_left (C : Type u₁) [Category.{v₁, u₁} C] [Limits.HasTerminal C] (X : C) : ((toOverTerminal C).obj X).left = X

def CategoryTheory.equivOverTerminal (C : Type u₁) [Category.{v₁, u₁} C] [Limits.HasTerminal C] : Over (⊤_ C) ≌ C

The slice category over the terminal object is equivalent to the original category.

Equations

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

theorem CategoryTheory.Over.star_map {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasBinaryProducts C] {X Y Z : C} (f : Y ⟶ Z) : (star X).map f = homMk (Limits.prod.map (CategoryStruct.id X) f) ⋯

instance CategoryTheory.Over.instIsLeftAdjointForgetOfHasBinaryProducts_poly {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasBinaryProducts C] (X : C) : (forget X).IsLeftAdjoint

Note that the binary products assumption is necessary: the existence of a right adjoint to Over.forget X is equivalent to the existence of each binary product X ⨯ -.

theorem CategoryTheory.Over.whiskerLeftProdMapId {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteLimits C] {X A A' : C} {g : A ⟶ A'} : MonoidalCategoryStruct.whiskerLeft X g = Limits.prod.map (CategoryStruct.id X) g

def CategoryTheory.Over.starForgetIsoTensorLeft {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteLimits C] (X : C) : (star X).comp (forget X) ≅ MonoidalCategory.tensorLeft X

Equations

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

@[simp]

theorem CategoryTheory.Over.forgetAdjStar.unit_app {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasBinaryProducts C] {I : C} (X : Over I) : (forgetAdjStar I).unit.app X = homMk (Limits.prod.lift X.hom (CategoryStruct.id X.left)) ⋯

@[simp]

theorem CategoryTheory.Over.forgetAdjStar.counit_app {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasBinaryProducts C] {I : C} (X : C) : (forgetAdjStar I).counit.app X = Limits.prod.snd

@[simp]

theorem CategoryTheory.Over.forgetAdjStar.homEquiv_homMk_lift {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasBinaryProducts C] {I : C} {X : Over I} {A : C} {f : X.left ⟶ A} : ((forgetAdjStar I).homEquiv X A) f = homMk (Limits.prod.lift X.hom f) ⋯

@[simp]

theorem CategoryTheory.Over.forgetAdjStar.homEquiv_left_lift {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasBinaryProducts C] {I : C} {X : Over I} {A : C} {f : X.left ⟶ A} : (((forgetAdjStar I).homEquiv X A) f).left = Limits.prod.lift X.hom f

theorem CategoryTheory.Over.forgetAdjStar.homEquiv_lift' {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasBinaryProducts C] {X I : C} {u : X ⟶ I} {A : C} {f : X ⟶ A} : ((forgetAdjStar I).homEquiv (mk u) A) f = homMk (Limits.prod.lift u f) ⋯

@[simp]

theorem CategoryTheory.Over.forgetAdjStar.homEquiv_symm_left_snd {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasBinaryProducts C] {I : C} {X : Over I} {A : C} {f : X ⟶ (star I).obj A} : ((forgetAdjStar I).homEquiv X A).symm f = CategoryStruct.comp f.left Limits.prod.snd

def CategoryTheory.Adjunction.equivalenceRightAdjointIsoInverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : D ≌ C) (R : Functor C D) (adj : e.functor ⊣ R) : R ≅ e.inverse

A right adjoint to the forward functor of an equivalence is naturally isomorphic to the inverse functor of the equivalence.

Equations

• CategoryTheory.Adjunction.equivalenceRightAdjointIsoInverse e R adj = (CategoryTheory.conjugateIsoEquiv adj e.toAdjunction) (CategoryTheory.Iso.refl e.functor)

def CategoryTheory.Over.starIsoToOverTerminal (C : Type u₁) [Category.{v₁, u₁} C] [Limits.HasTerminal C] [Limits.HasBinaryProducts C] : star (⊤_ C) ≅ Functor.toOverTerminal C

star (⊤_ C) : C ⥤ Over (⊤_ C) is naturally isomorphic to Functor.toOverTerminal C.

Equations

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

def CategoryTheory.Over.starPullbackIsoStar {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasBinaryProducts C] [Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) : (star Y).comp (pullback f) ≅ star X

A natural isomorphism between the functors star X and star Y ⋙ pullback f for any morphism f : X ⟶ Y.

Equations

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

theorem CategoryTheory.Over.iteratedSliceBackward_forget {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (A : Over X) : A.iteratedSliceBackward.comp (forget A) = map A.hom

def CategoryTheory.Over.starIteratedSliceForwardIsoPullback {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteWidePullbacks C] {X Y : C} (f : X ⟶ Y) : (star (mk f)).comp (mk f).iteratedSliceForward ≅ pullback f

The functor Over.pullback f : Over Y ⥤ Over X is naturally isomorphic to Over.star : Over Y ⥤ Over (Over.mk f) post-composed with the iterated slice equivlanece Over (Over.mk f) ⥤ Over X.

Equations

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