Some basic equalities and isomorphisms of composition and base change functors

Notation

We provide the following notations:

Given a morphism f : J ⟶ I in a category C,

• Σ_ f is the functor Over.map f : Over I ⥤ Over J.
• Δ_ f is the functor baseChange f : Over J ⥤ Over I.

Given an object I : C,

• Σ_ I is the functor Over.forget : Over I ⥤ C.
• Δ_ I is the functor Over.star : C ⥤ Over I.

For X Y : Over I,

• μ_ X Y is the projection morphism (Σ_ X.hom).obj ((Δ_ X.hom).obj Y) ⟶ Y defined via the counit of the adjunction Σ_ ⊣ Δ_, namely (mapAdjunction Y.hom).counit.app.
• π_ X Y is the projection morphism (Σ_ X.hom).obj ((Δ_ X.hom).obj Y) ⟶ X defined via the counit of the adjunction Σ_ ⊣ Δ_ and the isomorphism swapIso X Y : (Σ_ X.hom).obj ((Δ_ X.hom).obj Y) ≅ (Σ_ Y.hom).obj ((Δ_ Y.hom).obj X).

We prove that μ_ X Y and π_ X Y form a pullback square:

  P ---- μ --> •
  |            |
  π            Y
  |            |
  v            v
  • ---X--->  I

Implementation Notes

(SH): The definitions Over.pullback and mapPullbackAdj already existed in mathlib. Later, Over.baseChange and Over.mapAdjunction were added which are duplicates, but the latter have additional simp lemmas, namely unit_app and counit_app which makes proving things with simp easier.

We might change instances of Over.mapAdjunction to Over.mapPullbackAdj.

(SH) : WIP -- adiding simp attributes to Over.forgetAdjStar. This means we no longer will need the lemmas in the namespace Over.forgetAdjStar.

Other diagrams

                      .fst
        pullback p f ------> X
          |                  |
          |                  | p
    .snd  |                  |
          v                  v
          J   ---------->    I
                    f

Using the notation above, we have

• hom_eq_pullback_snd proves that (Δ_ f Over.mk p).hom is pullback.snd
• natIsoTensorLeft proves that Δ_ f ⋙ Σ_ f is isomorphic to the product functor f × _ in the slice category Over I.

def CategoryTheory.«termΣ__» : Lean.ParserDescr

A morphism f : X ⟶ Y induces a functor Over X ⥤ Over Y in the obvious way.

See https://stacks.math.columbia.edu/tag/001G.

Equations

• CategoryTheory.«termΣ__» = Lean.ParserDescr.node `CategoryTheory.termΣ__ 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "Σ_ ") (Lean.ParserDescr.cat `term 90))

def CategoryTheory.«termΣ___1» : Lean.ParserDescr

The forgetful functor mapping an arrow to its domain.

See https://stacks.math.columbia.edu/tag/001G.

Equations

• CategoryTheory.«termΣ___1» = Lean.ParserDescr.node `CategoryTheory.termΣ___1 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "Σ_ ") (Lean.ParserDescr.cat `term 90))

def CategoryTheory.termΔ__ : Lean.ParserDescr

Given a morphism f : X ⟶ Y, the functor baseChange f takes morphisms over Y to morphisms over X via pullbacks.

Equations

• CategoryTheory.termΔ__ = Lean.ParserDescr.node `CategoryTheory.termΔ__ 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "Δ_ ") (Lean.ParserDescr.cat `term 90))

def CategoryTheory.termΔ___1 : Lean.ParserDescr

The functor from C to Over X which sends Y : C to π₁ : X ⨯ Y ⟶ X, sometimes denoted X*.

Equations

• CategoryTheory.termΔ___1 = Lean.ParserDescr.node `CategoryTheory.termΔ___1 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "Δ_ ") (Lean.ParserDescr.cat `term 90))

@[simp]

theorem CategoryTheory.Over.forgetAdjStar.unit_app_left_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasBinaryProducts C] {I : C} (X : CategoryTheory.Over I) : ((CategoryTheory.Over.forgetAdjStar I).unit.app X).left = CategoryTheory.Limits.prod.lift X.hom (CategoryTheory.CategoryStruct.id X.left)

@[simp]

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

@[simp]

def CategoryTheory.Over.forgetAdjStar.counit_app_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasBinaryProducts C] {I : C} (X : C) : (CategoryTheory.Over.forgetAdjStar I).counit.app X = CategoryTheory.Limits.prod.snd

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

theorem CategoryTheory.Over.forgetAdjStar.homEquiv_symm {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {I : C} [CategoryTheory.Limits.HasBinaryProducts C] (X : CategoryTheory.Over I) (A : C) (f : X ⟶ (Δ_ I).obj A) : ((CategoryTheory.Over.forgetAdjStar I).homEquiv X A).symm f = CategoryTheory.CategoryStruct.comp f.left CategoryTheory.Limits.prod.snd

@[simp]

theorem CategoryTheory.WhiskeringNaturality {C : Type u_1} [CategoryTheory.Category.{u_6, u_1} C] {A : Type u_2} {B : Type u_3} [CategoryTheory.Category.{u_5, u_2} A] [CategoryTheory.Category.{u_4, u_3} B] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor A B} {H : CategoryTheory.Functor B C} {K : CategoryTheory.Functor B C} (α : F ⟶ G) (β : H ⟶ K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight α H) (CategoryTheory.whiskerLeft G β) = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft F β) (CategoryTheory.whiskerRight α K)

@[simp]

theorem CategoryTheory.pullback.map_id {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {S : C} (f : W ⟶ S) (g : X ⟶ S) [CategoryTheory.Limits.HasPullback f g] (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id W) f) (h' : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) g) : CategoryTheory.Limits.pullback.map f g f g (CategoryTheory.CategoryStruct.id W) (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id S) h h' = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f g)

@[simp]

theorem CategoryTheory.Over.eqToHom_left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {U : CategoryTheory.Over X} {V : CategoryTheory.Over X} (e : U = V) : (CategoryTheory.eqToHom e).left = CategoryTheory.eqToHom ⋯

theorem CategoryTheory.Over.mapForget_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : X ⟶ Y) : (Σ_ f).comp (Σ_ Y) = Σ_ X

def CategoryTheory.Over.mapForgetIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : X ⟶ Y) : (Σ_ f).comp (Σ_ Y) ≅ Σ_ X

Equality of functors should be avoided if possible, instead we use the isomorphism version. For use elsewhere.

Equations

• CategoryTheory.Over.mapForgetIso f = CategoryTheory.eqToIso ⋯

theorem CategoryTheory.Over.mapComp_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (Σ_ f).comp (Σ_ g) = Σ_ CategoryTheory.CategoryStruct.comp f g

def CategoryTheory.Over.mapCompIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (Σ_ f).comp (Σ_ g) ≅ Σ_ CategoryTheory.CategoryStruct.comp f g

Equations

• CategoryTheory.Over.mapCompIso f g = CategoryTheory.eqToIso ⋯

theorem CategoryTheory.baseChange.obj_hom_eq_pullback_snd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} {J : C} (f : J ⟶ I) (X : CategoryTheory.Over I) : ((Δ_ f).obj X).hom = CategoryTheory.Limits.pullback.snd

For an arrow f : J ⟶ I and an object X : Over I, the base-change of X along f is pullback.snd.

theorem CategoryTheory.baseChange.Over.star_obj_eq_mk_prod_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasBinaryProducts C] (I : C) (X : C) : (Δ_ I).obj X = CategoryTheory.Over.mk CategoryTheory.Limits.prod.fst

def CategoryTheory.baseChange.terminal_from {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (I : C) (X : CategoryTheory.Over (⊤_ C)) : (Δ_ CategoryTheory.Limits.terminal.from I).obj X ≅ (Δ_ I).obj X.left

The base-change along terminal.from ER: Changed statement from an equality to an isomorphism. Proof of commutativity is stuck because of the rewrite. Perhaps I can do this another way?

Equations

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

@[simp]

theorem CategoryTheory.baseChange.swapIso_inv_right_down_down {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} (X : CategoryTheory.Over I) (Y : CategoryTheory.Over I) : ⋯ = ⋯

@[simp]

theorem CategoryTheory.baseChange.swapIso_hom_left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} (X : CategoryTheory.Over I) (Y : CategoryTheory.Over I) : (CategoryTheory.baseChange.swapIso X Y).hom.left = (CategoryTheory.Limits.pullbackSymmetry Y.hom X.hom).hom

@[simp]

theorem CategoryTheory.baseChange.swapIso_hom_right_down_down {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} (X : CategoryTheory.Over I) (Y : CategoryTheory.Over I) : ⋯ = ⋯

@[simp]

theorem CategoryTheory.baseChange.swapIso_inv_left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} (X : CategoryTheory.Over I) (Y : CategoryTheory.Over I) : (CategoryTheory.baseChange.swapIso X Y).inv.left = (CategoryTheory.Limits.pullbackSymmetry Y.hom X.hom).inv

def CategoryTheory.baseChange.swapIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} (X : CategoryTheory.Over I) (Y : CategoryTheory.Over I) : (Σ_ X.hom).obj ((Δ_ X.hom).obj Y) ≅ (Σ_ Y.hom).obj ((Δ_ Y.hom).obj X)

Equations

• CategoryTheory.baseChange.swapIso X Y = CategoryTheory.Over.isoMk (CategoryTheory.Limits.pullbackSymmetry Y.hom X.hom) ⋯

@[simp]

theorem CategoryTheory.baseChange.swap_eq_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} {X : CategoryTheory.Over I} {Y : CategoryTheory.Over I} : ((Σ_ X.hom).obj ((Δ_ X.hom).obj Y)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry Y.hom X.hom).hom ((Σ_ Y.hom).obj ((Δ_ Y.hom).obj X)).hom

def CategoryTheory.baseChange.projFst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} (X : CategoryTheory.Over I) (Y : CategoryTheory.Over I) : (Σ_ X.hom).obj ((Δ_ X.hom).obj Y) ⟶ Y

For X Y : Over I, the map μ := projFst, defined via the counit of the adjunction Σ_ ⊣ Δ_, is a morphism form the base-change of Y along X to Y .

  P ---- μ --> •
  |            |
  π            Y
  |            |
  v            v
  • ---X--->  I

Equations

• CategoryTheory.baseChange.projFst X Y = (CategoryTheory.Over.mapAdjunction X.hom).counit.app Y

def CategoryTheory.baseChange.projSnd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} (X : CategoryTheory.Over I) (Y : CategoryTheory.Over I) : (Σ_ X.hom).obj ((Δ_ X.hom).obj Y) ⟶ X

For X Y : Over I, the map π := projSnd is a morphism form the base-change of X along Y to X.

  P ---- μ --> •
  |            |
  π            Y
  |            |
  v            v
  • ---X--->  I

Equations

• CategoryTheory.baseChange.projSnd X Y = CategoryTheory.CategoryStruct.comp (CategoryTheory.baseChange.swapIso X Y).hom ((CategoryTheory.Over.mapAdjunction Y.hom).counit.app X)

theorem CategoryTheory.baseChange.projFst_eq_pullback_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} {X : CategoryTheory.Over I} {Y : CategoryTheory.Over I} : CategoryTheory.baseChange.projFst X Y = CategoryTheory.Over.homMk (id CategoryTheory.Limits.pullback.fst) ⋯

theorem CategoryTheory.baseChange.projFst_left_eq_pullback_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} {X : CategoryTheory.Over I} {Y : CategoryTheory.Over I} : (CategoryTheory.baseChange.projFst X Y).left = CategoryTheory.Limits.pullback.fst

theorem CategoryTheory.baseChange.projSnd_eq_pullback_snd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} {X : CategoryTheory.Over I} {Y : CategoryTheory.Over I} : CategoryTheory.baseChange.projSnd X Y = CategoryTheory.Over.homMk (id CategoryTheory.Limits.pullback.snd) ⋯

theorem CategoryTheory.baseChange.projSnd_left_eq_pullback_snd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} {X : CategoryTheory.Over I} {Y : CategoryTheory.Over I} : (CategoryTheory.baseChange.projSnd X Y).left = CategoryTheory.Limits.pullback.snd

def CategoryTheory.baseChange.isBinaryProduct {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} (X : CategoryTheory.Over I) (Y : CategoryTheory.Over I) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.baseChange.projSnd X Y) (CategoryTheory.baseChange.projFst X Y))

Equations

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

@[simp]

theorem CategoryTheory.baseChange.isoProd_hom_right {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} (X : CategoryTheory.Over I) (Y : CategoryTheory.Over I) [CategoryTheory.Limits.HasBinaryProduct X Y] : (CategoryTheory.baseChange.isoProd X Y).hom.right = CategoryTheory.CategoryStruct.id ((Σ_ X.hom).obj ((Δ_ X.hom).obj Y)).right

@[simp]

theorem CategoryTheory.baseChange.isoProd_hom_left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} (X : CategoryTheory.Over I) (Y : CategoryTheory.Over I) [CategoryTheory.Limits.HasBinaryProduct X Y] : (CategoryTheory.baseChange.isoProd X Y).hom.left = (CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.pair X Y) (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.comp (CategoryTheory.baseChange.swapIso X Y).hom ((CategoryTheory.Over.mapAdjunction Y.hom).counit.app X)) ((CategoryTheory.Over.mapAdjunction X.hom).counit.app Y))).left

@[simp]

theorem CategoryTheory.baseChange.isoProd_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} (X : CategoryTheory.Over I) (Y : CategoryTheory.Over I) [CategoryTheory.Limits.HasBinaryProduct X Y] : (CategoryTheory.baseChange.isoProd X Y).inv = (CategoryTheory.baseChange.isBinaryProduct X Y).lift (CategoryTheory.Limits.BinaryFan.mk CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd)

def CategoryTheory.baseChange.isoProd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} (X : CategoryTheory.Over I) (Y : CategoryTheory.Over I) [CategoryTheory.Limits.HasBinaryProduct X Y] : (Σ_ X.hom).obj ((Δ_ X.hom).obj Y) ≅ X ⨯ Y

The object (Σ_ X.hom) ((Δ_ X.hom) Y) is isomorphic to the binary product X × Y in Over I.

Equations

• CategoryTheory.baseChange.isoProd X Y = (CategoryTheory.baseChange.isBinaryProduct X Y).conePointUniqueUpToIso (CategoryTheory.Limits.prodIsProd X Y)

def CategoryTheory.baseChange.isoProdmk {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} {J : C} (f : J ⟶ I) (Y : CategoryTheory.Over I) [CategoryTheory.Limits.HasBinaryProduct (CategoryTheory.Over.mk f) Y] : (Σ_ f).obj ((Δ_ f).obj Y) ≅ CategoryTheory.Over.mk f ⨯ Y

Equations

• CategoryTheory.baseChange.isoProdmk f Y = CategoryTheory.baseChange.isoProd (CategoryTheory.Over.mk f) Y

@[simp]

theorem CategoryTheory.baseChange.isoProd_comp_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} (X : CategoryTheory.Over I) (Y : CategoryTheory.Over I) [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.baseChange.isoProd X Y).hom CategoryTheory.Limits.prod.fst = CategoryTheory.baseChange.projSnd X Y

@[simp]

theorem CategoryTheory.baseChange.isoProdmk_comp_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} {J : C} (f : J ⟶ I) (Y : CategoryTheory.Over I) [CategoryTheory.Limits.HasBinaryProduct (CategoryTheory.Over.mk f) Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.baseChange.isoProdmk f Y).hom CategoryTheory.Limits.prod.fst = CategoryTheory.baseChange.projSnd (CategoryTheory.Over.mk f) Y

@[simp]

theorem CategoryTheory.baseChange.isoProd_comp_snd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} {X : CategoryTheory.Over I} {Y : CategoryTheory.Over I} [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.baseChange.isoProd X Y).hom CategoryTheory.Limits.prod.snd = CategoryTheory.baseChange.projFst X Y

def CategoryTheory.baseChange.natIsoTensorLeft {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] {I : C} (X : CategoryTheory.Over I) : (Δ_ X.hom).comp (Σ_ X.hom) ≅ CategoryTheory.MonoidalCategory.tensorLeft X

The functor composition (baseChange X.hom) ⋙ (Over.map X.hom) is naturally isomorphic to the left tensor product functor X × _

Equations

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

def CategoryTheory.baseChange.natIsoTensorLeftOverMk {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] {I : C} {J : C} (f : J ⟶ I) : (Δ_ f).comp (Σ_ f) ≅ CategoryTheory.MonoidalCategory.tensorLeft (CategoryTheory.Over.mk f)

Equations

• CategoryTheory.baseChange.natIsoTensorLeftOverMk f = CategoryTheory.baseChange.natIsoTensorLeft (CategoryTheory.Over.mk f)

def CategoryTheory.baseChange.mapStarIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} (f : X ⟶ Y) : Δ_ X ≅ (Δ_ Y).comp (Δ_ f)

The isomorphism between the base change functors obtained as the conjugate of the mapForgetIso. For use elsewhere.

Equations

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

def CategoryTheory.baseChange.id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) : Δ_ CategoryTheory.CategoryStruct.id I ≅ CategoryTheory.Functor.id (CategoryTheory.Over I)

Equations

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

def CategoryTheory.baseChange.comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : Δ_ CategoryTheory.CategoryStruct.comp f g ≅ (Δ_ g).comp (Δ_ f)

The conjugate isomorphism between pullback functors.

Equations

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

@[simp]

theorem CategoryTheory.Limits.pullback.map_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W : C} {X : C} {S : C} (f : W ⟶ S) (g : X ⟶ S) [CategoryTheory.Limits.HasPullback f g] (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id W) f) (h' : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) g) : CategoryTheory.Limits.pullback.map f g f g (CategoryTheory.CategoryStruct.id W) (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id S) h h' = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f g)

@[simp]

theorem CategoryTheory.toOverTerminal'_map {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] (T : C) (h : CategoryTheory.Limits.IsTerminal T) : ∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.toOverTerminal' T h).map f = CategoryTheory.Over.homMk f ⋯

@[simp]

theorem CategoryTheory.toOverTerminal'_obj {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] (T : C) (h : CategoryTheory.Limits.IsTerminal T) (X : C) : (CategoryTheory.toOverTerminal' T h).obj X = CategoryTheory.Over.mk (h.from X)

def CategoryTheory.toOverTerminal' {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] (T : C) (h : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Functor C (CategoryTheory.Over T)

Equations

• CategoryTheory.toOverTerminal' T h = { obj := fun (X : C) => CategoryTheory.Over.mk (h.from X), map := fun {X Y : C} (f : X ⟶ Y) => CategoryTheory.Over.homMk f ⋯, map_id := ⋯, map_comp := ⋯ }

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

Note (SH): the difference between this and Δ_ (⊤_ C) is that we only use the assumption that C has only terminal but not binary products. On the other hand, I recommend using Δ_ (⊤_ C) in general since we know more facts about it such its adjunction (top of the file).

Equations

• CategoryTheory.toOverTerminal = CategoryTheory.toOverTerminal' (⊤_ C) CategoryTheory.Limits.terminalIsTerminal

def CategoryTheory.equivOverTerminal' {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] (T : C) (h : CategoryTheory.Limits.IsTerminal T) : C ≌ CategoryTheory.Over T

Equations

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

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

Equations

• CategoryTheory.equivOverTerminal = CategoryTheory.equivOverTerminal' (⊤_ C) CategoryTheory.Limits.terminalIsTerminal

def CategoryTheory.isoOverTerminal {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Cat.of (ULift.{u_3, u_2} C) ≅ CategoryTheory.Cat.of (CategoryTheory.Over (⊤_ C))

Equations

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

def CategoryTheory.toOverTerminalStarIso {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] : Δ_ ⊤_ C ≅ CategoryTheory.toOverTerminal

Equations

• CategoryTheory.toOverTerminalStarIso = let_fun this := CategoryTheory.Iso.refl (Σ_ ⊤_ C); sorryAx (Δ_ ⊤_ C ≅ CategoryTheory.toOverTerminal)

def CategoryTheory.toOverTerminalStarTriangleIso {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) : Δ_ X ≅ CategoryTheory.toOverTerminal.comp (Δ_ CategoryTheory.Limits.terminal.from X)

Equations

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