mathlib documentation

category_theory.comm_sq

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, 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.

source
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.

source
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'
source
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) :
category_theory.comm_sq g f i h
source
theorem category_theory.comm_sq.of_arrow {C : Type u_1} [category_theory.category C] {f g : category_theory.arrow C} (h : f ⟶ g) :
category_theory.comm_sq f.hom h.left h.right g.hom
source
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) :
category_theory.comm_sq i.op h.op g.op f.op

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

source
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) :
category_theory.comm_sq i.unop h.unop g.unop f.unop

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

source
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)
source
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.

source
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
source
@[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
source
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
source
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
source
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
source
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) :
_.lift_struct

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

Equations
source
@[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
source
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) :
_.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
source
@[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
source
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) :
sq.lift_struct ≃ _.lift_struct

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

Equations
source
@[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) :
⇑((category_theory.comm_sq.lift_struct.op_equiv sq).symm) l = l.unop
source
@[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) :
⇑(category_theory.comm_sq.lift_struct.op_equiv sq) l = l.op
source
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) :
sq.lift_struct ≃ _.lift_struct

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

Equations
source
@[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] :
subsingleton sq.lift_struct
source
@[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] :
subsingleton sq.lift_struct
source
@[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
source
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) :
sq.has_lift
source
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) :
sq.has_lift ↔ nonempty sq.lift_struct
source
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) :
sq.has_lift ↔ _.has_lift
source
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) :
sq.has_lift ↔ _.has_lift
source
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
source
@[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
source
@[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'
source
@[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
source
@[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'