Documentation

Mathlib.CategoryTheory.CommSq

Commutative squares #

This file provide an API for commutative squares in categories. If top, left, right and bottom are four morphisms which are the edges of a square, CommSq top left right bottom is the predicate that this square is commutative.

The structure CommSq is extended in CategoryTheory/Shapes/Limits/CommSq.lean as IsPullback and IsPushout in order to define pullback and pushout squares.

Future work #

Refactor LiftStruct from Arrow.lean and lifting properties using CommSq.lean.

structure CategoryTheory.CommSq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : W Y) (h : X Z) (i : Y Z) :

The proposition that a square

  W ---f---> X
  |          |
  g          h
  |          |
  v          v
  Y ---i---> Z

is a commuting square.

Instances For
    theorem CategoryTheory.CommSq.w_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z✝} {i : Y Z✝} (self : CategoryTheory.CommSq f g h✝ i) {Z : C} (h : Z✝ Z) :
    theorem CategoryTheory.CommSq.flip {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : CategoryTheory.CommSq f g h i) :
    theorem CategoryTheory.CommSq.op {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : CategoryTheory.CommSq f g h i) :
    CategoryTheory.CommSq i.op h.op g.op f.op

    The commutative square in the opposite category associated to a commutative square.

    theorem CategoryTheory.CommSq.unop {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W : Cᵒᵖ} {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : CategoryTheory.CommSq f g h i) :
    CategoryTheory.CommSq i.unop h.unop g.unop f.unop

    The commutative square associated to a commutative square in the opposite category.

    theorem CategoryTheory.CommSq.vert_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {i : Y Z} {g : W Y} {h : X Z} (p : CategoryTheory.CommSq f g.hom h.hom i) :
    CategoryTheory.CommSq i g.inv h.inv f
    theorem CategoryTheory.Functor.map_commSq {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : CategoryTheory.CommSq f g h i) :
    CategoryTheory.CommSq (F.map f) (F.map g) (F.map h) (F.map i)
    theorem CategoryTheory.CommSq.map {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : CategoryTheory.CommSq f g h i) :
    CategoryTheory.CommSq (F.map f) (F.map g) (F.map h) (F.map i)

    Alias of CategoryTheory.Functor.map_commSq.

    theorem CategoryTheory.CommSq.LiftStruct.ext_iff {C : Type u_1} :
    ∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : CategoryTheory.CommSq f i p g} (x y : CategoryTheory.CommSq.LiftStruct sq), x = y x.l = y.l
    theorem CategoryTheory.CommSq.LiftStruct.ext {C : Type u_1} :
    ∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : CategoryTheory.CommSq f i p g} (x y : CategoryTheory.CommSq.LiftStruct sq), x.l = y.lx = y
    structure CategoryTheory.CommSq.LiftStruct {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : CategoryTheory.CommSq f i p g) :
    Type u_2

    Now we consider a square:

      A ---f---> X
      |          |
      i          p
      |          |
      v          v
      B ---g---> Y
    

    The datum of a lift in a commutative square, i.e. an up-right-diagonal morphism which makes both triangles commute.

    Instances For
      @[simp]
      theorem CategoryTheory.CommSq.LiftStruct.op_l {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : CategoryTheory.CommSq f i p g} (l : CategoryTheory.CommSq.LiftStruct sq) :
      def CategoryTheory.CommSq.LiftStruct.op {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : CategoryTheory.CommSq f i p g} (l : CategoryTheory.CommSq.LiftStruct sq) :

      A LiftStruct for a commutative square gives a LiftStruct for the corresponding square in the opposite category.

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.CommSq.LiftStruct.unop_l {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A : Cᵒᵖ} {B : Cᵒᵖ} {X : Cᵒᵖ} {Y : Cᵒᵖ} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : CategoryTheory.CommSq f i p g} (l : CategoryTheory.CommSq.LiftStruct sq) :

        A LiftStruct for a commutative square in the opposite category gives a LiftStruct for the corresponding square in the original category.

        Equations
        Instances For
          def CategoryTheory.CommSq.LiftStruct.opEquiv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : CategoryTheory.CommSq f i p g) :

          Equivalences of LiftStruct for a square and the corresponding square in the opposite category.

          Equations
          Instances For

            Equivalences of LiftStruct for a square in the oppositive category and the corresponding square in the original category.

            Equations
            Instances For
              instance CategoryTheory.CommSq.subsingleton_liftStruct_of_epi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : CategoryTheory.CommSq f i p g) [CategoryTheory.Epi i] :
              Equations
              • =
              instance CategoryTheory.CommSq.subsingleton_liftStruct_of_mono {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : CategoryTheory.CommSq f i p g) [CategoryTheory.Mono p] :
              Equations
              • =
              class CategoryTheory.CommSq.HasLift {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : CategoryTheory.CommSq f i p g) :

              The assertion that a square has a LiftStruct.

              Instances
                theorem CategoryTheory.CommSq.HasLift.mk' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : CategoryTheory.CommSq f i p g} (l : CategoryTheory.CommSq.LiftStruct sq) :
                theorem CategoryTheory.CommSq.HasLift.iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : CategoryTheory.CommSq f i p g) :
                theorem CategoryTheory.CommSq.HasLift.iff_op {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : CategoryTheory.CommSq f i p g) :
                noncomputable def CategoryTheory.CommSq.lift {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : CategoryTheory.CommSq f i p g) [hsq : CategoryTheory.CommSq.HasLift sq] :
                B X

                A choice of a diagonal morphism that is part of a LiftStruct when the square has a lift.

                Equations
                Instances For
                  @[simp]
                  theorem CategoryTheory.CommSq.fac_left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : CategoryTheory.CommSq f i p g) [hsq : CategoryTheory.CommSq.HasLift sq] :
                  @[simp]
                  theorem CategoryTheory.CommSq.fac_right {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : CategoryTheory.CommSq f i p g) [hsq : CategoryTheory.CommSq.HasLift sq] :