mathlib3 documentation

category_theory.comm_sq

Commutative squares #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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, comm_sq top left right bottom is the predicate that this square is commutative.

The structure comm_sq is extended in category_theory/shapes/limits/comm_sq.lean as is_pullback and is_pushout in order to define pullback and pushout squares.

Future work #

Refactor lift_struct from arrow.lean and lifting properties using comm_sq.lean.

structure category_theory.comm_sq {C : Type u_1} [category_theory.category C] {W X Y Z : C} (f : W X) (g : W Y) (h : X Z) (i : Y Z) :
Prop

The proposition that a square

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

is a commuting square.

theorem category_theory.comm_sq.w_assoc {C : Type u_1} [category_theory.category C] {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (self : category_theory.comm_sq f g h i) {X' : C} (f' : Z X') :
f h f' = g i f'
theorem category_theory.comm_sq.flip {C : Type u_1} [category_theory.category C] {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : category_theory.comm_sq f g h i) :
theorem category_theory.comm_sq.op {C : Type u_1} [category_theory.category C] {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : category_theory.comm_sq f g h i) :

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

theorem category_theory.comm_sq.unop {C : Type u_1} [category_theory.category C] {W X Y Z : Cᵒᵖ} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : category_theory.comm_sq f g h i) :

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

theorem category_theory.functor.map_comm_sq {C : Type u_1} [category_theory.category C] {D : Type u_3} [category_theory.category D] (F : C D) {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : category_theory.comm_sq f g h i) :
category_theory.comm_sq (F.map f) (F.map g) (F.map h) (F.map i)
theorem category_theory.comm_sq.map {C : Type u_1} [category_theory.category C] {D : Type u_3} [category_theory.category D] (F : C D) {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : category_theory.comm_sq f g h i) :
category_theory.comm_sq (F.map f) (F.map g) (F.map h) (F.map i)

Alias of category_theory.functor.map_comm_sq.

theorem category_theory.comm_sq.lift_struct.ext_iff {C : Type u_1} {_inst_1 : category_theory.category C} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : category_theory.comm_sq f i p g} (x y : sq.lift_struct) :
x = y x.l = y.l
@[nolint, ext]
structure category_theory.comm_sq.lift_struct {C : Type u_1} [category_theory.category C] {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : category_theory.comm_sq f i p g) :
Type u_2
  • l : B X
  • fac_left' : i self.l = f
  • fac_right' : self.l p = g

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

Instances for category_theory.comm_sq.lift_struct
theorem category_theory.comm_sq.lift_struct.ext {C : Type u_1} {_inst_1 : category_theory.category C} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : category_theory.comm_sq f i p g} (x y : sq.lift_struct) (h : x.l = y.l) :
x = y
theorem category_theory.comm_sq.lift_struct.fac_left {C : Type u_1} [category_theory.category C] {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : category_theory.comm_sq f i p g} (self : sq.lift_struct) :
i self.l = f
theorem category_theory.comm_sq.lift_struct.fac_right {C : Type u_1} [category_theory.category C] {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : category_theory.comm_sq f i p g} (self : sq.lift_struct) :
self.l p = g
def category_theory.comm_sq.lift_struct.op {C : Type u_1} [category_theory.category C] {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : category_theory.comm_sq f i p g} (l : sq.lift_struct) :

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

Equations
@[simp]
theorem category_theory.comm_sq.lift_struct.op_l {C : Type u_1} [category_theory.category C] {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : category_theory.comm_sq f i p g} (l : sq.lift_struct) :
l.op.l = l.l.op
def category_theory.comm_sq.lift_struct.unop {C : Type u_1} [category_theory.category C] {A B X Y : Cᵒᵖ} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : category_theory.comm_sq f i p g} (l : sq.lift_struct) :

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

Equations
@[simp]
theorem category_theory.comm_sq.lift_struct.unop_l {C : Type u_1} [category_theory.category C] {A B X Y : Cᵒᵖ} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : category_theory.comm_sq f i p g} (l : sq.lift_struct) :
l.unop.l = l.l.unop
def category_theory.comm_sq.lift_struct.op_equiv {C : Type u_1} [category_theory.category C] {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : category_theory.comm_sq f i p g) :

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

Equations
@[simp]
theorem category_theory.comm_sq.lift_struct.op_equiv_symm_apply {C : Type u_1} [category_theory.category C] {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : category_theory.comm_sq f i p g) (l : _.lift_struct) :
@[simp]
theorem category_theory.comm_sq.lift_struct.op_equiv_apply {C : Type u_1} [category_theory.category C] {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : category_theory.comm_sq f i p g) (l : sq.lift_struct) :
def category_theory.comm_sq.lift_struct.unop_equiv {C : Type u_1} [category_theory.category C] {A B X Y : Cᵒᵖ} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : category_theory.comm_sq f i p g) :

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

Equations
@[protected, instance]
def category_theory.comm_sq.subsingleton_lift_struct_of_epi {C : Type u_1} [category_theory.category C] {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : category_theory.comm_sq f i p g) [category_theory.epi i] :
@[protected, instance]
def category_theory.comm_sq.subsingleton_lift_struct_of_mono {C : Type u_1} [category_theory.category C] {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : category_theory.comm_sq f i p g) [category_theory.mono p] :
@[class]
structure category_theory.comm_sq.has_lift {C : Type u_1} [category_theory.category C] {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : category_theory.comm_sq f i p g) :
Prop

The assertion that a square has a lift_struct.

Instances of this typeclass
theorem category_theory.comm_sq.has_lift.mk' {C : Type u_1} [category_theory.category C] {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : category_theory.comm_sq f i p g} (l : sq.lift_struct) :
theorem category_theory.comm_sq.has_lift.iff {C : Type u_1} [category_theory.category C] {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : category_theory.comm_sq f i p g) :
theorem category_theory.comm_sq.has_lift.iff_op {C : Type u_1} [category_theory.category C] {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : category_theory.comm_sq f i p g) :
theorem category_theory.comm_sq.has_lift.iff_unop {C : Type u_1} [category_theory.category C] {A B X Y : Cᵒᵖ} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : category_theory.comm_sq f i p g) :
noncomputable def category_theory.comm_sq.lift {C : Type u_1} [category_theory.category C] {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : category_theory.comm_sq f i p g) [hsq : sq.has_lift] :
B X

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

Equations
@[simp]
theorem category_theory.comm_sq.fac_left {C : Type u_1} [category_theory.category C] {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : category_theory.comm_sq f i p g) [hsq : sq.has_lift] :
i sq.lift = f
@[simp]
theorem category_theory.comm_sq.fac_left_assoc {C : Type u_1} [category_theory.category C] {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : category_theory.comm_sq f i p g) [hsq : sq.has_lift] {X' : C} (f' : X X') :
i sq.lift f' = f f'
@[simp]
theorem category_theory.comm_sq.fac_right {C : Type u_1} [category_theory.category C] {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : category_theory.comm_sq f i p g) [hsq : sq.has_lift] :
sq.lift p = g
@[simp]
theorem category_theory.comm_sq.fac_right_assoc {C : Type u_1} [category_theory.category C] {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : category_theory.comm_sq f i p g) [hsq : sq.has_lift] {X' : C} (f' : Y X') :
sq.lift p f' = g f'