Documentation

Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.BeckChevalley

Beck-Chevalley natural transformations and natural isomorphisms #

We construct the so-called Beck-Chevalley natural transformations and isomorphisms through the repeated applications of the mate construction in the vertical and horizontal directions.

Main declarations #

Over.mapIsoSquare: The isomorphism between the functors Over.map h ⋙ Over.map g and Over.map f ⋙ Over.map k for a commutative square of morphisms h ≫ g = f ≫ k.
Over.pullbackMapTwoSquare: The Beck-Chevalley natural transformation of a commutative square of morphisms h ≫ g = f ≫ k.
Over.pullbackForgetTriangle: The natural transformation pullback f ⋙ forget X ⟶ forget Y.
Over.pullbackIsoSquare: The isomorphism between the pullbacks along a commutative square of morphisms h ≫ g = f ≫ k.
Over.pushforwardBeckChevalleySquare: The Beck-Chevalley natural transformation for a commutative square of morphisms h ≫ g = f ≫ k in the slice category Over Y.
Over.pushforwardSquareIso: The isomorphism between the pushforwards along a commutative square of morphisms h ≫ g = f ≫ k.

Implementation notes #

The lax naturality squares are constructed by the mate equivalence mateEquiv and the natural iso-squares are constructed by the more special conjugation equivalence conjugateIsoEquiv.

References #

The methodology and the notation of the successive mate constructions to obtain the Beck-Chevalley natural transformations and isomorphisms are based on the following paper:

[A 2-categorical proof of Frobenius for fibrations defined from a generic point, in Mathematical Structures in Computer Science, 2024][Hazratpour_Riehl_2024]

theorem CategoryTheory.Over.map_square_eq {C : Type u} [Category.{v, u} C] {X Y Z W : C} {h : X ⟶ Z} {f : X ⟶ Y} {g : Z ⟶ W} {k : Y ⟶ W} (sq : CommSq h f g k := by aesop) :

(map h).comp (map g) = (map f).comp (map k)

def CategoryTheory.Over.mapIsoSquare {C : Type u} [Category.{v, u} C] {X Y Z W : C} {h : X ⟶ Z} {f : X ⟶ Y} {g : Z ⟶ W} {k : Y ⟶ W} (sq : CommSq h f g k := by aesop) :

(map h).comp (map g) ≅ (map f).comp (map k)

Promoting the equality mapSquare_eq of functors to an isomorphism.

        Over X -- .map h -> Over Z
           |                  |
   .map f  |         ≅        | .map g
           ↓                  ↓
        Over Y -- .map k -> Over W

The Beck Chevalley transformations are iterated mates of this isomorphism in the horizontal and vertical directions.

Equations

CategoryTheory.Over.mapIsoSquare sq = CategoryTheory.eqToIso ⋯

Instances For

def CategoryTheory.Over.pullbackMapTwoSquare {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y Z W : C} (h : X ⟶ Z) (f : X ⟶ Y) (g : Z ⟶ W) (k : Y ⟶ W) (sq : CommSq h f g k) :

TwoSquare (pullback f) (map k) (map h) (pullback g)

The Beck-Chevalley natural transformation pullback f ⋙ map h ⟶ map k ⋙ pullback g constructed as a mate of mapIsoSquare:

    Over Y - pullback f → Over X
      |                     |
map k |          ↙          | map h
      ↓                     ↓
    Over W - pullback g → Over Z

Equations

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

Instances For

def CategoryTheory.Over.pullbackForgetTwoSquare {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) :

TwoSquare (pullback f) (forget Y) (forget X) (Functor.id C)

The natural transformation pullback f ⋙ forget X ⟶ forget Y ⋙ 𝟭 C as the mate of the isomorphism mapForget f:

       Over Y - pullback f → Over X
         |                     |
forget Y |          ↙          | forget X
         ↓                     ↓
         C ======== 𝟭 ======== C

Equations

CategoryTheory.Over.pullbackForgetTwoSquare f = (CategoryTheory.mateEquiv (CategoryTheory.Over.mapPullbackAdj f) CategoryTheory.Adjunction.id) (CategoryTheory.Over.mapForget f).inv

Instances For

theorem CategoryTheory.Over.isCartesian_pullbackForgetTwoSquare {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) :

NatTrans.IsCartesian (pullbackForgetTwoSquare f)

def CategoryTheory.Over.pullbackForgetTriangle {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) :

(pullback f).comp (forget X) ⟶ forget Y

The natural transformation pullback f ⋙ forget X ⟶ forget Y, a variant of pullbackForgetTwoSquare.

Equations

CategoryTheory.Over.pullbackForgetTriangle f = CategoryTheory.Over.pullbackForgetTwoSquare f

Instances For

def CategoryTheory.Over.pullbackMapTriangle {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y Z : C} (h : X ⟶ Z) (f : X ⟶ Y) (h' : Y ⟶ Z) (w : CategoryStruct.comp f h' = h) :

(pullback f).comp (map h) ⟶ map h'

The natural transformation pullback f ⋙ map h ⟶ map h' for a triangle f : h ⟶ h'.

Equations

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

Instances For

def CategoryTheory.Over.pullbackIsoSquare {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y Z W : C} (h : X ⟶ Z) (f : X ⟶ Y) (g : Z ⟶ W) (k : Y ⟶ W) (sq : CommSq h f g k) :

(pullback k).comp (pullback f) ≅ (pullback g).comp (pullback h)

The isomorphism between the pullbacks along a commutative square. This is constructed as the conjugate of the mapIsoSquare.

          Over X ←--.pullback h-- Over Z
             ↑                       ↑
.pullback f  |          ≅            | .pullback g
             |                       |
          Over Y ←--.pullback k-- Over W

Equations

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

Instances For

def CategoryTheory.Over.pushforwardPullbackTwoSquare {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y Z W : C} (h : X ⟶ Z) (f : X ⟶ Y) (g : Z ⟶ W) (k : Y ⟶ W) (sq : CommSq h f g k) [ExponentiableMorphism f] [ExponentiableMorphism g] :

TwoSquare (ExponentiableMorphism.pushforward g) (pullback h) (pullback k) (ExponentiableMorphism.pushforward f)

The Beck-Chevalley natural transformation pushforward g ⋙ pullback k ⟶ pullback h ⋙ pushforward f constructed as a mate of pullbackMapTwoSquare.

         Over Z - pushforward g → Over W
           |                        |
pullback h |           ↙            | pullback k
           ↓                        ↓
         Over X - pushforward f → Over Y

Equations

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

Instances For

def CategoryTheory.Over.starPushforwardTriangle {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) [Limits.HasBinaryProducts C] [ExponentiableMorphism f] :

star Y ⟶ (star X).comp (ExponentiableMorphism.pushforward f)

A variant of pushforwardTwoSquare involving star instead of pullback.

Equations

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

Instances For

def CategoryTheory.Over.pushforwardIsoSquare {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y Z W : C} (h : X ⟶ Z) (f : X ⟶ Y) (g : Z ⟶ W) (k : Y ⟶ W) (sq : CommSq h f g k) [ExponentiableMorphism f] [ExponentiableMorphism g] [ExponentiableMorphism h] [ExponentiableMorphism k] :

(ExponentiableMorphism.pushforward h).comp (ExponentiableMorphism.pushforward g) ≅ (ExponentiableMorphism.pushforward f).comp (ExponentiableMorphism.pushforward k)

The conjugate isomorphism between the pushforwards along a commutative square.

            Over X --.pushforward h -→ Over Z
               |                        |
.pushforward f |           ≅            | .pushforward g
               ↓                        ↓
            Over Y --.pushforward k -→ Over W

Equations

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

Instances For

theorem CategoryTheory.IsPullback.left_face_of_comm_cube {C : Type u} [Category.{v, u} C] {P W X Y Q Z S T : C} (p₁ : P ⟶ W) (p₂ : P ⟶ X) (f₁ : W ⟶ S) (f₂ : X ⟶ S) (q₁ : Q ⟶ Y) (q₂ : Q ⟶ Z) (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T) (i₄ : P ⟶ Q) (sq_top : CommSq p₂ i₄ i₂ q₂) (sq_bot : CommSq f₁ i₁ i₃ g₁) (sq_left : CommSq i₄ p₁ q₁ i₁) (pb_back : IsPullback p₂ p₁ f₂ f₁) (pb_front : IsPullback q₂ q₁ g₂ g₁) (pb_right : IsPullback i₂ f₂ g₂ i₃) :

IsPullback i₄ p₁ q₁ i₁

In a commutative cube diagram if the front, back and the right face are pullback squares then the the left face is also a pullback square.

          P ---p₂------  X
         /|             /|
    i₄  / |       i₂   / |
       /  |           /  | f₂
      Q ----q₂-----  Z   |
      |   |          |   |
      |   W -f₁----- | - S
  q₁  |  /           |  /
      | / i₁         | / i₃
      |/             |/
      Y ----g₁------ T

theorem CategoryTheory.IsPullback.back_face_of_comm_cube {C : Type u} [Category.{v, u} C] {P W X Y Q Z S T : C} (p₁ : P ⟶ W) (p₂ : P ⟶ X) (f₁ : W ⟶ S) (f₂ : X ⟶ S) (q₁ : Q ⟶ Y) (q₂ : Q ⟶ Z) (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T) (i₄ : P ⟶ Q) (sq_top : CommSq p₂ i₄ i₂ q₂) (sq_bot : CommSq f₁ i₁ i₃ g₁) (sq_back : CommSq p₂ p₁ f₂ f₁) (pb_front : IsPullback q₂ q₁ g₂ g₁) (pb_left : IsPullback i₄ p₁ q₁ i₁) (pb_right : IsPullback i₂ f₂ g₂ i₃) :

IsPullback p₂ p₁ f₂ f₁

In a commutative cube diagram if the front, the left and the right face are pullback squares then the the back face is also a pullback square.

          P ---p₂------  X
         /|             /|
    i₄  / |       i₂   / |
       /  |           /  | f₂
      Q ----q₂-----  Z   |
      |   |          |   |
      |   W -f₁----- | - S
  q₁  |  /           |  /
      | / i₁         | / i₃
      |/             |/
      Y ----g₁------ T

theorem CategoryTheory.IsPullback.pullback.map_isIso_of_pullback_right_of_comm_cube {C : Type u} [Category.{v, u} C] {W X Y Z S T : C} (f₁ : W ⟶ S) (f₂ : X ⟶ S) [Limits.HasPullback f₁ f₂] (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) [Limits.HasPullback g₁ g₂] (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T) (sq_bot : CommSq f₁ i₁ i₃ g₁) [IsIso i₁] (pb_right : IsPullback i₂ f₂ g₂ i₃) :

IsIso (Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ ⋯ ⋯)

The pullback comparison map pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ between two pullback squares is an isomorphism if i₁ is an isomorphism and one of the connecting morphisms is an isomorphism.

theorem CategoryTheory.mapPullbackAdj.counit_app_left {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y : C} {f : X ⟶ Y} (A : Over Y) :

((Over.mapPullbackAdj f).counit.app A).left = Limits.pullback.fst A.hom f

@[simp]

theorem CategoryTheory.pullbackMapTwoSquare_app {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y Z W : C} {h : X ⟶ Z} {f : X ⟶ Y} {g : Z ⟶ W} {k : Y ⟶ W} (sq : CommSq h f g k) (A : Over Y) :

(Over.pullbackMapTwoSquare h f g k sq).app A = Over.homMk (Limits.pullback.map A.hom f (CategoryStruct.comp A.hom k) g (CategoryStruct.id ((Functor.id C).obj A.left)) h k ⋯ ⋯) ⋯

theorem CategoryTheory.forget_map_pullbackMapTwoSquare {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y Z W : C} {h : X ⟶ Z} {f : X ⟶ Y} {g : Z ⟶ W} {k : Y ⟶ W} (sq : CommSq h f g k) (A : Over Y) :

(Over.forget Z).map ((Over.pullbackMapTwoSquare h f g k sq).app A) = Limits.pullback.map A.hom f (CategoryStruct.comp A.hom k) g (CategoryStruct.id ((Functor.id C).obj A.left)) h k ⋯ ⋯

theorem CategoryTheory.isIso_forgetMappullbackMapTwoSquare_of_isPullback {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y Z W : C} {h : X ⟶ Z} {f : X ⟶ Y} {g : Z ⟶ W} {k : Y ⟶ W} (A : Over Y) (pb : IsPullback h f g k) :

IsIso ((Over.forget Z).map ((Over.pullbackMapTwoSquare h f g k ⋯).app A))

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

IsIso (Over.pullbackMapTwoSquare h f g k ⋯)

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

def CategoryTheory.pullbackMapIsoSquare {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y Z W : C} {h : X ⟶ Z} {f : X ⟶ Y} {g : Z ⟶ W} {k : Y ⟶ W} (pb : IsPullback h f g k) :

(Over.pullback f).comp (Over.map h) ≅ (Over.map k).comp (Over.pullback g)

The pullback-map exchange isomorphism.

Equations

CategoryTheory.pullbackMapIsoSquare pb = CategoryTheory.asIso (CategoryTheory.Over.pullbackMapTwoSquare h f g k ⋯)

Instances For

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

IsIso (Over.pushforwardPullbackTwoSquare h f g k ⋯)

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

def CategoryTheory.pushforwardPullbackIsoSquare {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y Z W : C} {h : X ⟶ Z} {f : X ⟶ Y} {g : Z ⟶ W} {k : Y ⟶ W} (pb : IsPullback h f g k) [ExponentiableMorphism f] [ExponentiableMorphism g] :

(ExponentiableMorphism.pushforward g).comp (Over.pullback k) ≅ (Over.pullback h).comp (ExponentiableMorphism.pushforward f)

The pullback-pushforward exchange isomorphism.

Equations

CategoryTheory.pushforwardPullbackIsoSquare pb = CategoryTheory.asIso (CategoryTheory.Over.pushforwardPullbackTwoSquare h f g k ⋯)

Instances For