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.
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') :
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
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
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.
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.
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) :
@[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
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
- category_theory.comm_sq.lift_struct.has_sizeof_inst
- category_theory.comm_sq.subsingleton_lift_struct_of_epi
- category_theory.comm_sq.subsingleton_lift_struct_of_mono
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) :
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) :
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.
@[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) :
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.
@[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) :
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
@[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
@[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) :
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
@[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
- exists_lift : nonempty sq.lift_struct
The assertion that a square has a lift_struct.
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
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
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] :
@[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] :