English
If a functor is fibered, and we have arrows that are Cartesian, then their composition is Cartesian: IsCartesian f φ and IsCartesian g ψ imply IsCartesian (f ≫ g) (φ ≫ ψ).
Русский
Если функтор является фиберированным, и стрелы являются картизанами, то их композиция является картизанской.
LaTeX
$$$[IsCartesian p f φ] \land [IsCartesian p g ψ] ⇒ IsCartesian p (f ≫ g) (φ ≫ ψ)$$$
Lean4
/-- In a category which admits strongly Cartesian pullbacks, any Cartesian morphism is
strongly Cartesian. This is a helper-lemma for the fact that admitting strongly Cartesian pullbacks
implies being fibered. -/
theorem isStronglyCartesian_of_exists_isCartesian (p : 𝒳 ⥤ 𝒮)
(h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳) (φ : b ⟶ a), IsStronglyCartesian p f φ) {R S : 𝒮} (f : R ⟶ S)
{a b : 𝒳} (φ : a ⟶ b) [p.IsCartesian f φ] : p.IsStronglyCartesian f φ :=
by
constructor
intro c g φ' hφ'
subst_hom_lift p f φ; clear a b R S
obtain ⟨a', ψ, hψ⟩ :=
h _ _
(p.map φ)
-- Let `τ' : c ⟶ a'` be the map induced by the universal property of `ψ`
let τ' := IsStronglyCartesian.map p (p.map φ) ψ (f' := g ≫ p.map φ) rfl φ'
let Φ := domainUniqueUpToIso p (p.map φ) φ ψ
use τ' ≫ Φ.hom
refine ⟨⟨by simp only [Φ]; infer_instance, ?_⟩, ?_⟩
·
simp [τ', Φ]
-- It remains to check that it is unique. This follows from the universal property of `ψ`.
intro π ⟨hπ, hπ_comp⟩
rw [← Iso.comp_inv_eq]
apply IsStronglyCartesian.map_uniq p (p.map φ) ψ rfl φ'
simp [hπ_comp, Φ]
