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.