Cartesian morphisms #
This file defines cartesian resp. strongly cartesian morphisms with respect to a functor
p : š³ ā„¤ š®.
This file has been adapted to Mathlib/CategoryTheory/FiberedCategory/Cocartesian.lean,
please try to change them in sync.
Main definitions #
IsCartesian p f Ļ expresses that Ļ is a cartesian morphism lying over f with respect to p in
the sense of SGA 1 VI 5.1. This means that for any morphism Ļ' : a' ā¶ b lying over f there is
a unique morphism Ļ : a' ā¶ a lying over š R, such that Ļ' = Ļ ā« Ļ.
IsStronglyCartesian p f Ļ expresses that Ļ is a strongly cartesian morphism lying over f with
respect to p, see https://stacks.math.columbia.edu/tag/02XK.
Implementation #
The constructor of IsStronglyCartesian has been named universal_property', and is mainly
intended to be used for constructing instances of this class. To use the universal property, we
generally recommended to use the lemma IsStronglyCartesian.universal_property instead. The
difference between the two is that the latter is more flexible with respect to non-definitional
equalities.
References #
A morphism Ļ : a ā¶ b in š³ lying over f : R ā¶ S in š® is cartesian if for all
morphisms Ļ' : a' ā¶ b, also lying over f, there exists a unique morphism Ļ : a' ā¶ a lifting
š R such that Ļ' = Ļ ā« Ļ.
See SGA 1 VI 5.1.
- cond : IsHomLiftAux p f Ļ
Instances
A morphism Ļ : a ā¶ b in š³ lying over f : R ā¶ S in š® is strongly cartesian if for
all morphisms Ļ' : a' ā¶ b and all diagrams of the form
a' a --Ļ--> b
| | |
v v v
R' --g--> R --f--> S
such that Ļ' lifts g ā« f, there exists a lift Ļ of g such that Ļ' = Ļ ā« Ļ.
- cond : IsHomLiftAux p f Ļ
Instances
Given a cartesian morphism Ļ : a ā¶ b lying over f : R ā¶ S in š³, and another morphism
Ļ' : a' ā¶ b which also lifts f, then IsCartesian.map f Ļ Ļ' is the morphism a' ā¶ a lifting
š R obtained from the universal property of Ļ.
Equations
- CategoryTheory.Functor.IsCartesian.map p f Ļ Ļ' = Classical.choose āÆ
Instances For
Given a cartesian morphism Ļ : a ā¶ b lying over f : R ā¶ S in š³, and another morphism
Ļ' : a' ā¶ b which also lifts f. Then any morphism Ļ : a' ā¶ a lifting š R such that
g ā« Ļ = Ļ' must equal the map induced from the universal property of Ļ.
Given a cartesian morphism Ļ : a ā¶ b lying over f : R ā¶ S in š³, and two morphisms
Ļ Ļ' : a' ā¶ a such that Ļ ā« Ļ = Ļ' ā« Ļ. Then we must have Ļ = Ļ'.
The canonical isomorphism between the domains of two cartesian arrows lying over the same object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Precomposing a cartesian morphism with an isomorphism lifting the identity is cartesian.
The universal property of a strongly cartesian morphism.
This lemma is more flexible with respect to non-definitional equalities than the field
universal_property' of IsStronglyCartesian.
Given a diagram
a' a --Ļ--> b
| | |
v v v
R' --g--> R --f--> S
such that Ļ is strongly cartesian, and a morphism Ļ' : a' ā¶ b. Then map is the map a' ā¶ a
lying over g obtained from the universal property of Ļ.
Equations
- CategoryTheory.Functor.IsStronglyCartesian.map p f Ļ hf' Ļ' = Classical.choose āÆ
Instances For
Given a diagram
a' a --Ļ--> b
| | |
v v v
R' --g--> R --f--> S
such that Ļ is strongly cartesian, and morphisms Ļ' : a' ā¶ b, Ļ : a' ā¶ a such that
Ļ ā« Ļ = Ļ'. Then Ļ is the map induced by the universal property.
Given a diagram
a' a --Ļ--> b
| | |
v v v
R' --g--> R --f--> S
such that Ļ is strongly cartesian, and morphisms Ļ Ļ' : a' ā¶ a such that
g ā« Ļ = Ļ' = g ā« Ļ'. Then we have that Ļ = Ļ'.
When its possible to compare the two, the composition of two IsStronglyCartesian.map will also
be given by a IsStronglyCartesian.map. In other words, given diagrams
a'' a' a --Ļ--> b
| | | |
v v v v
R'' --g'--> R' --g--> R --f--> S
and
a' --Ļ'--> b
| |
v v
R' --f'--> S
and
a'' --Ļ''--> b
| |
v v
R'' --f''--> S
such that Ļ and Ļ' are strongly cartesian morphisms, and such that f' = g ā« f and
f'' = g' ā« f'. Then composing the induced map from a'' ā¶ a' with the induced map from
a' ā¶ a gives the induced map from a'' ā¶ a.
Given two strongly cartesian morphisms Ļ, Ļ as follows
a --Ļ--> b --Ļ--> c
| | |
v v v
R --f--> S --g--> T
Then the composite Ļ ā« Ļ is also strongly cartesian.
Given two commutative squares
a --Ļ--> b --Ļ--> c
| | |
v v v
R --f--> S --g--> T
such that Ļ ā« Ļ and Ļ are strongly cartesian, then so is Ļ.
A strongly cartesian morphism lying over an isomorphism is an isomorphism.
The canonical isomorphism between the domains of two strongly cartesian morphisms lying over isomorphic objects.
Equations
- One or more equations did not get rendered due to their size.