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 {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) :

    The square commutes.

    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.CommSq.horiz_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W : C} {X : C} {Y : C} {Z : C} {g : W Y} {h : X Z} {f : W X} {i : Y Z} (p : CategoryTheory.CommSq f.hom g h i.hom) :
    CategoryTheory.CommSq f.inv h g i.inv
    theorem CategoryTheory.CommSq.horiz_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W : C} {X : C} {X' : C} {Y : C} {Z : C} {Z' : C} {f : W X} {f' : X X'} {g : W Y} {h : X Z} {h' : X' Z'} {i : Y Z} {i' : Z Z'} (hsq₁ : CategoryTheory.CommSq f g h i) (hsq₂ : CategoryTheory.CommSq f' h h' i') :

    The horizontal composition of two commutative squares as below is a commutative square.

      W ---f---> X ---f'--> X'
      |          |          |
      g          h          h'
      |          |          |
      v          v          v
      Y ---i---> Z ---i'--> Z'
    
    
    theorem CategoryTheory.CommSq.vert_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W : C} {X : C} {Y : C} {Y' : C} {Z : C} {Z' : C} {f : W X} {g : W Y} {g' : Y Y'} {h : X Z} {h' : Z Z'} {i : Y Z} {i' : Y' Z'} (hsq₁ : CategoryTheory.CommSq f g h i) (hsq₂ : CategoryTheory.CommSq i g' h' i') :

    The vertical composition of two commutative squares as below is a commutative square.

      W ---f---> X
      |          |
      g          h
      |          |
      v          v
      Y ---i---> Z
      |          |
      g'         h'
      |          |
      v          v
      Y'---i'--> Z'
    
    
    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 {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 : sq.LiftStruct}, x.l = y.lx = y
    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 : sq.LiftStruct}, x = y x.l = y.l
    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
      theorem CategoryTheory.CommSq.LiftStruct.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} (self : sq.LiftStruct) :

      The upper left triangle commutes.

      theorem CategoryTheory.CommSq.LiftStruct.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} (self : sq.LiftStruct) :

      The lower right triangle commutes.

      @[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 : sq.LiftStruct) :
      l.op.l = l.l.op
      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 : sq.LiftStruct) :
      .LiftStruct

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

      Equations
      • l.op = { l := l.l.op, fac_left := , fac_right := }
      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 : sq.LiftStruct) :
        l.unop.l = l.l.unop
        def CategoryTheory.CommSq.LiftStruct.unop {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 : sq.LiftStruct) :
        .LiftStruct

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

        Equations
        • l.unop = { l := l.l.unop, fac_left := , fac_right := }
        Instances For
          @[simp]
          theorem CategoryTheory.CommSq.LiftStruct.opEquiv_symm_apply {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 : .LiftStruct) :
          @[simp]
          theorem CategoryTheory.CommSq.LiftStruct.opEquiv_apply {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 : sq.LiftStruct) :
          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) :
          sq.LiftStruct .LiftStruct

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

          Equations
          Instances For
            def CategoryTheory.CommSq.LiftStruct.unopEquiv {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) :
            sq.LiftStruct .LiftStruct

            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] :
              Subsingleton sq.LiftStruct
              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] :
              Subsingleton sq.LiftStruct
              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.exists_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} [self : sq.HasLift] :
                Nonempty sq.LiftStruct

                Square has a LiftStruct.

                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 : sq.LiftStruct) :
                sq.HasLift
                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) :
                sq.HasLift Nonempty sq.LiftStruct
                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) :
                sq.HasLift .HasLift
                theorem CategoryTheory.CommSq.HasLift.iff_unop {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) :
                sq.HasLift .HasLift
                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 : sq.HasLift] :
                B X

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

                Equations
                • sq.lift = .some.l
                Instances For
                  @[simp]
                  theorem CategoryTheory.CommSq.fac_left_assoc {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 : sq.HasLift] {Z : C} (h : X Z) :
                  @[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 : sq.HasLift] :
                  @[simp]
                  theorem CategoryTheory.CommSq.fac_right_assoc {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 : sq.HasLift] {Z : C} (h : Y Z) :
                  @[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 : sq.HasLift] :