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.
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.
comm_sq is extended in
is_pushout in order to define pullback and pushout squares.
Future work #
arrow.lean and lifting properties using
The commutative square in the opposite category associated to a commutative square.
The commutative square associated to a commutative square in the opposite category.
The datum of a lift in a commutative square, i.e. a up-right-diagonal morphism which makes both triangles commute.
lift_struct for a commutative square gives a
lift_struct for the
corresponding square in the opposite category.
lift_struct for a commutative square in the opposite category
lift_struct for the corresponding square in the original category.
lift_struct for a square and the corresponding square
in the opposite category.
lift_struct for a square in the oppositive category and
the corresponding square in the original category.
- exists_lift : nonempty sq.lift_struct
The assertion that a square has a
A choice of a diagonal morphism that is part of a
the square has a lift.