English
The object function of the fiber inclusion is injective: two objects in the fiber that have the same underlying object in the ambient category are equal.
Русский
Функция отображения объектов включения фибры инъективна: если два объекта в фибре имеют одинаковый базовый объект в окружающей категории, они равны.
LaTeX
$$$(fiberInclusion).obj\;\text{Injective}$$$
Lean4
/-- In a fibered category, any Cartesian morphism is strongly Cartesian. -/
instance isStronglyCartesian_of_isCartesian (p : 𝒳 ⥤ 𝒮) [p.IsFibered] {R S : 𝒮} (f : R ⟶ S) {a b : 𝒳} (φ : a ⟶ b)
[p.IsCartesian f φ] : p.IsStronglyCartesian f φ where
universal_property' g φ'
hφ' := by
-- Let `ψ` be a Cartesian arrow lying over `g`
let ψ := pullbackMap (domain_eq p f φ) g
let τ := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
use τ ≫ ψ
refine
⟨⟨inferInstance, by simp only [assoc, IsCartesian.fac, τ]⟩, ?_⟩
-- It remains to check that `τ ≫ ψ` is unique.
-- So fix another lift `π` of `g` satisfying `π ≫ φ = φ'`.
intro π
⟨hπ, hπ_comp⟩
-- Write `π` as `π = τ' ≫ ψ` for some `τ'` induced by the universal property of `ψ`.
rw [← fac p g ψ π]
-- It remains to show that `τ' = τ`. This follows again from the universal property of `ψ`.
congr 1
apply map_uniq
rwa [← assoc, IsCartesian.fac]
