Documentation

Poly.LCCC.BeckChevalley

Beck-Chevalley natural transformations and natural isomorphisms #

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

The Beck Chevalley transformations are iterated mates of this isomorphism.

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

      The Beck-Chevalley natural transformation.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def CategoryTheory.Over.pullbackSquareIso {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {W X Y Z : C} (f : W X) (g : X Z) (h : W Y) (k : Y Z) (w : CategoryStruct.comp f g = 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.
        Instances For

          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.
          Instances For

            The conjugate isomorphism between the pushforwards along a commutative square.

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

              Calculating the counit components of mapAdjunction.

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

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

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

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