Cartesian morphisms #
This file defines cartesian resp. strongly cartesian morphisms in a based category.
Main definitions #
IsCartesian p f φ
expresses that φ
is a cartesian arrow 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 φ' = τ ≫ φ
.
References #
The proposition that a morphism φ : a ⟶ b
in 𝒳
lying over f : R ⟶ S
in 𝒮
is a
cartesian arrow, see SGA 1 VI 5.1.
- cond : CategoryTheory.IsHomLiftAux p f φ
- universal_property : ∀ {a' : 𝒳} (φ' : a' ⟶ b) [inst : p.IsHomLift f φ'], ∃! χ : a' ⟶ a, p.IsHomLift (CategoryTheory.CategoryStruct.id R) χ ∧ CategoryTheory.CategoryStruct.comp χ φ = φ'
Instances
Given a cartesian arrow φ : a ⟶ b
lying over f : R ⟶ S
in 𝒳
, a morphism φ' : a' ⟶ b
lifting 𝟙 R
, then IsCartesian.map f φ φ'
is the morphism a' ⟶ a
obtained from the universal
property of φ
.
Equations
Instances For
Equations
- ⋯ = ⋯
Given a cartesian arrow φ : a ⟶ b
lying over f : R ⟶ S
in 𝒳
, a morphism φ' : a' ⟶ b
lifting 𝟙 R
, and a morphism ψ : a' ⟶ a
such that g ≫ ψ = φ'
. Then ψ
is the map induced
by the universal property of φ
.
Given a cartesian arrow φ : a ⟶ b
lying over f : R ⟶ S
in 𝒳
, a morphism φ' : a' ⟶ b
lifting 𝟙 R
, and two morphisms ψ ψ' : a' ⟶ a
such that g ≫ ψ = φ' = g ≫ ψ'
. 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.
Equations
- ⋯ = ⋯
Postcomposing a cartesian morphism with an isomorphism lifting the identity is cartesian.
Equations
- ⋯ = ⋯