Beck-Chevalley natural transformations and natural isomorphisms

theorem CategoryTheory.Over.mapSquare_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : X ⟶ Z) (h : W ⟶ Y) (k : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp h k) : (Σ_ f).comp (Σ_ g) = (Σ_ h).comp (Σ_ k)

def CategoryTheory.Over.mapSquareIso {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : X ⟶ Z) (h : W ⟶ Y) (k : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp h k) : (Σ_ f).comp (Σ_ g) ≅ (Σ_ h).comp (Σ_ k)

The Beck Chevalley transformations are iterated mates of this isomorphism.

Equations

• CategoryTheory.Over.mapSquareIso f g h k w = CategoryTheory.eqToIso ⋯

def CategoryTheory.Over.mapSquareIso' {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : X ⟶ Z) (h : W ⟶ Y) (k : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp h k) : (Σ_ f).comp (Σ_ g) ≅ (Σ_ h).comp (Σ_ k)

Equations

• CategoryTheory.Over.mapSquareIso' f g h k w = ⋯.mpr (CategoryTheory.Iso.refl ((Σ_ h).comp (Σ_ k)))

def CategoryTheory.Over.pullbackBeckChevalleyNatTrans {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : X ⟶ Z) (h : W ⟶ Y) (k : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp h k) : (Δ_ h).comp (Σ_ f) ⟶ (Σ_ k).comp (Δ_ g)

The Beck-Chevalley natural transformation.

Equations

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

def CategoryTheory.Over.pullbackBeckChevalleyOfMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} (f : X ⟶ Y) : (Δ_ f).comp (Σ_ X) ⟶ Σ_ Y

Equations

• CategoryTheory.Over.pullbackBeckChevalleyOfMap f = (CategoryTheory.mateEquiv (CategoryTheory.Over.mapPullbackAdj f) CategoryTheory.Adjunction.id) (⋯.mp (CategoryTheory.Over.mapForgetIso f).inv)

def CategoryTheory.Over.pullbackSquareIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : X ⟶ Z) (h : W ⟶ Y) (k : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp h k) : (Δ_ k).comp (Δ_ h) ≅ (Δ_ g).comp (Δ_ f)

The conjugate isomorphism between the pullbacks along a commutative square.

Equations

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

def CategoryTheory.Over.pushforwardBeckChevalleyNatTrans {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : X ⟶ Z) (h : W ⟶ Y) (k : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp h k) (gexp : CartesianExponentiable g) (hexp : CartesianExponentiable h) : (Π_ g).comp (Δ_ k) ⟶ (Δ_ f).comp (Π_ h)

The Beck-Chevalley natural transformations in a square of pullbacks and pushforwards.

Equations

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

def CategoryTheory.Over.pushforwardSquareIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : X ⟶ Z) (h : W ⟶ Y) (k : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp h k) (fexp : CartesianExponentiable f) (gexp : CartesianExponentiable g) (hexp : CartesianExponentiable h) (kexp : CartesianExponentiable k) : (Π_ f).comp (Π_ g) ≅ (Π_ h).comp (Π_ k)

The conjugate isomorphism between the pushforwards along a commutative square.

Equations

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

theorem CategoryTheory.mapPullbackAdj.counit.app_pullback.fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} (f : X ⟶ Y) (y : CategoryTheory.Over Y) : ((CategoryTheory.Over.mapPullbackAdj f).counit.app y).left = CategoryTheory.Limits.pullback.fst y.hom f

Calculating the counit components of mapAdjunction.

def CategoryTheory.pullbackNatTrans.app.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : X ⟶ Z) (h : W ⟶ Y) (k : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp h k) (y : CategoryTheory.Over Y) : (Σ_ X).obj (((Δ_ h).comp (Σ_ f)).obj y) ⟶ (Σ_ X).obj (((Σ_ k).comp (Δ_ g)).obj y)

Equations

• CategoryTheory.pullbackNatTrans.app.map f g h k w y = CategoryTheory.Limits.pullback.map y.hom h (CategoryTheory.CategoryStruct.comp y.hom k) g (CategoryTheory.CategoryStruct.id y.left) f k ⋯ ⋯

theorem CategoryTheory.pullbackBeckChevalleyComponent_pullbackMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : X ⟶ Z) (h : W ⟶ Y) (k : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp h k) (y : CategoryTheory.Over Y) : (Σ_ X).map ((CategoryTheory.Over.pullbackBeckChevalleyNatTrans f g h k w).app y) = CategoryTheory.pullbackNatTrans.app.map f g h k w y

theorem CategoryTheory.pullbackNatTrans_of_IsPullback_component_is_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : X ⟶ Z) (h : W ⟶ Y) (k : Y ⟶ Z) (pb : CategoryTheory.IsPullback f h g k) (y : CategoryTheory.Over Y) : CategoryTheory.IsIso ((Σ_ X).map ((CategoryTheory.Over.pullbackBeckChevalleyNatTrans f g h k ⋯).app y))

instance CategoryTheory.pullbackBeckChevalleyNatTrans_of_IsPullback_is_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : X ⟶ Z) (h : W ⟶ Y) (k : Y ⟶ Z) (pb : CategoryTheory.IsPullback f h g k) : CategoryTheory.IsIso (CategoryTheory.Over.pullbackBeckChevalleyNatTrans f g h k ⋯)

The pullback Beck-Chevalley natural transformation of a pullback square is an isomorphism.

Equations

• ⋯ = ⋯

instance CategoryTheory.pushforwardBeckChevalleyNatTrans_of_IsPullback_is_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : X ⟶ Z) (h : W ⟶ Y) (k : Y ⟶ Z) (pb : CategoryTheory.IsPullback f h g k) (gexp : CartesianExponentiable g) (hexp : CartesianExponentiable h) : CategoryTheory.IsIso (CategoryTheory.Over.pushforwardBeckChevalleyNatTrans f g h k ⋯ gexp hexp)

The pushforward Beck-Chevalley natural transformation of a pullback square is an isomorphism.

Equations

• ⋯ = ⋯

instance CategoryTheory.pushforwardBeckChevalleyNatTrans_of_isPullback_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : X ⟶ Z) (h : W ⟶ Y) (k : Y ⟶ Z) (pb : CategoryTheory.IsPullback f h g k) (gexp : CartesianExponentiable g) (hexp : CartesianExponentiable h) : CategoryTheory.IsIso (CategoryTheory.Over.pushforwardBeckChevalleyNatTrans f g h k ⋯ gexp hexp)

The pushforward Beck-Chevalley natural transformation of a pullback square is an isomorphism.

Equations

• ⋯ = ⋯