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 Σ_ ⊣ Δ_.
• π_ X Y is the projection morphism (Σ_ X.hom).obj ((Δ_ X.hom).obj Y) ⟶ X defined via the counit of the adjunction Σ_ ⊣ Δ_ and the isomorphism (Σ_ 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) : WIP -- adding 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.

Stacks 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.

Stacks 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

In a category with pullbacks, a morphism f : X ⟶ Y induces a functor Over Y ⥤ Over X, by pulling back a morphism along f.

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} [Category.{u_2, u_1} C] [Limits.HasBinaryProducts C] {I : C} (X : Over I) : ((forgetAdjStar I).unit.app X).left = Limits.prod.lift X.hom (CategoryStruct.id X.left)

@[simp]

theorem CategoryTheory.Over.forgetAdjStar.unit_app_eq {C : Type u_1} [Category.{u_2, u_1} 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]

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

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Over.forgetAdjStar.homEquiv {C : Type u_1} [Category.{u_2, u_1} 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_symm {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasBinaryProducts C] {I : C} (X : Over I) (A : C) (f : X ⟶ (Δ_ I).obj A) : ((forgetAdjStar I).homEquiv X A).symm f = CategoryStruct.comp f.left Limits.prod.snd

@[simp]

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

def CategoryTheory.Over.mapForgetIso {C : Type u_1} [Category.{u_2, u_1} C] {X 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 ⋯

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

Equations

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

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

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} [Category.{u_2, u_1} C] [Limits.HasBinaryProducts C] (I X : C) : (Δ_ I).obj X = Over.mk Limits.prod.fst

def CategoryTheory.baseChange.terminal_from {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] [Limits.HasTerminal C] [Limits.HasBinaryProducts C] (I : C) (X : Over (⊤_ C)) : (Δ_ 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.

def CategoryTheory.baseChange.swapIso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {I : C} (X Y : 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.swapIso_inv_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {I : C} (X Y : Over I) : (swapIso X Y).inv.left = (Limits.pullbackSymmetry Y.hom X.hom).inv

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.baseChange.projFst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {I : C} (X Y : 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.mapPullbackAdj X.hom).counit.app Y

def CategoryTheory.baseChange.projSnd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {I : C} (X Y : 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.mapPullbackAdj Y.hom).counit.app X)

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

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

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

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

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

Equations

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

def CategoryTheory.baseChange.isoProd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {I : C} (X Y : Over I) [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)

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.baseChange.isoProdmk {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {I J : C} (f : J ⟶ I) (Y : Over I) [Limits.HasBinaryProduct (Over.mk f) Y] : (Σ_ f).obj ((Δ_ f).obj Y) ≅ 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} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {I : C} (X Y : Over I) [Limits.HasBinaryProduct X Y] : CategoryStruct.comp (isoProd X Y).hom Limits.prod.fst = projSnd X Y

@[simp]

theorem CategoryTheory.baseChange.isoProd_comp_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {I : C} (X Y : Over I) [Limits.HasBinaryProduct X Y] {Z : Over ((Functor.fromPUnit I).obj X.right)} (h : X ⟶ Z) : CategoryStruct.comp (isoProd X Y).hom (CategoryStruct.comp Limits.prod.fst h) = CategoryStruct.comp (projSnd X Y) h

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.baseChange.isoProd_comp_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {I : C} {X Y : Over I} [Limits.HasBinaryProduct X Y] {Z : Over ((Functor.fromPUnit I).obj X.right)} (h : Y ⟶ Z) : CategoryStruct.comp (isoProd X Y).hom (CategoryStruct.comp Limits.prod.snd h) = CategoryStruct.comp (projFst X Y) h

def CategoryTheory.baseChange.natIsoTensorLeft {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] [Limits.HasFiniteWidePullbacks C] {I : C} (X : Over I) : (Δ_ X.hom).comp (Σ_ X.hom) ≅ 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} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] [Limits.HasFiniteWidePullbacks C] {I J : C} (f : J ⟶ I) : (Δ_ f).comp (Σ_ f) ≅ MonoidalCategory.tensorLeft (Over.mk f)

Equations

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

def CategoryTheory.baseChange.mapStarIso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasBinaryProducts C] [Limits.HasPullbacks C] {X 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} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] (I : C) : Δ_ CategoryStruct.id I ≅ Functor.id (Over I)

Equations

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

def CategoryTheory.baseChange.comp {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : Δ_ 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.

def CategoryTheory.toOverTerminal' {C : Type u_2} [Category.{u_3, u_2} C] (T : C) (h : Limits.IsTerminal T) : Functor C (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 := ⋯ }

@[simp]

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

@[simp]

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

def CategoryTheory.toOverTerminal {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasTerminal C] : Functor C (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} [Category.{u_3, u_2} C] (T : C) (h : Limits.IsTerminal T) : C ≌ Over T

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• CategoryTheory.toOverTerminalStarIso = sorry

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

Equations

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