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

• A. Grothendieck, M. Raynaud, SGA 1

class CategoryTheory.Functor.IsCartesian {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) extends CategoryTheory.Functor.IsHomLift : Prop

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 χ φ = φ'

theorem CategoryTheory.Functor.IsCartesian.universal_property {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) {φ : a ⟶ b} [self : p.IsCartesian f φ] {a' : 𝒳} (φ' : a' ⟶ b) [p.IsHomLift f φ'] : ∃! χ : a' ⟶ a, p.IsHomLift (CategoryTheory.CategoryStruct.id R) χ ∧ CategoryTheory.CategoryStruct.comp χ φ = φ'

noncomputable def CategoryTheory.Functor.IsCartesian.map {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : 𝒳} (φ' : a' ⟶ b) [p.IsHomLift f φ'] : a' ⟶ a

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

• CategoryTheory.Functor.IsCartesian.map p f φ φ' = Classical.choose ⋯

instance CategoryTheory.Functor.IsCartesian.map_isHomLift {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : 𝒳} (φ' : a' ⟶ b) [p.IsHomLift f φ'] : p.IsHomLift (CategoryTheory.CategoryStruct.id R) (CategoryTheory.Functor.IsCartesian.map p f φ φ')

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Functor.IsCartesian.fac_assoc {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : 𝒳} (φ' : a' ⟶ b) [p.IsHomLift f φ'] {Z : 𝒳} (h : b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsCartesian.map p f φ φ') (CategoryTheory.CategoryStruct.comp φ h) = CategoryTheory.CategoryStruct.comp φ' h

@[simp]

theorem CategoryTheory.Functor.IsCartesian.fac {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : 𝒳} (φ' : a' ⟶ b) [p.IsHomLift f φ'] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsCartesian.map p f φ φ') φ = φ'

theorem CategoryTheory.Functor.IsCartesian.map_uniq {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : 𝒳} (φ' : a' ⟶ b) [p.IsHomLift f φ'] (ψ : a' ⟶ a) [p.IsHomLift (CategoryTheory.CategoryStruct.id R) ψ] (hψ : CategoryTheory.CategoryStruct.comp ψ φ = φ') : ψ = CategoryTheory.Functor.IsCartesian.map p f φ φ'

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 φ.

theorem CategoryTheory.Functor.IsCartesian.eq_of_fac {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : 𝒳} (φ' : a' ⟶ b) [p.IsHomLift f φ'] {ψ : a' ⟶ a} {ψ' : a' ⟶ a} [p.IsHomLift (CategoryTheory.CategoryStruct.id R) ψ] [p.IsHomLift (CategoryTheory.CategoryStruct.id R) ψ'] (hcomp : CategoryTheory.CategoryStruct.comp ψ φ = φ') (hcomp' : CategoryTheory.CategoryStruct.comp ψ' φ = φ') : ψ = ψ'

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 ψ = ψ'.

@[simp]

theorem CategoryTheory.Functor.IsCartesian.map_self {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] : CategoryTheory.Functor.IsCartesian.map p f φ φ = CategoryTheory.CategoryStruct.id a

@[simp]

theorem CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso_hom {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : 𝒳} (φ' : a' ⟶ b) [p.IsCartesian f φ'] : (CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso p f φ φ').hom = CategoryTheory.Functor.IsCartesian.map p f φ φ'

@[simp]

theorem CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso_inv {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : 𝒳} (φ' : a' ⟶ b) [p.IsCartesian f φ'] : (CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso p f φ φ').inv = CategoryTheory.Functor.IsCartesian.map p f φ' φ

noncomputable def CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : 𝒳} (φ' : a' ⟶ b) [p.IsCartesian f φ'] : a' ≅ a

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.

instance CategoryTheory.Functor.IsCartesian.of_iso_comp {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : 𝒳} (φ' : a' ≅ a) [p.IsHomLift (CategoryTheory.CategoryStruct.id R) φ'.hom] : p.IsCartesian f (CategoryTheory.CategoryStruct.comp φ'.hom φ)

Precomposing a cartesian morphism with an isomorphism lifting the identity is cartesian.

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.IsCartesian.of_comp_iso {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {b' : 𝒳} (φ' : b ≅ b') [p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ'.hom] : p.IsCartesian f (CategoryTheory.CategoryStruct.comp φ φ'.hom)

Postcomposing a cartesian morphism with an isomorphism lifting the identity is cartesian.

Equations

• ⋯ = ⋯