English
Given a lift φ′ of g ∘ f from a′ to ⟨S, a⟩, there is a canonical morphism from a′ to the Cartesian lift domainCartesianLift(a, f) whose base component is g and whose fiber component is constructed from φ′ by composing with the relevant isomorphisms coming from the pseudofunctor F. This morphism is explicitly defined by base = g and fiber = φ′.fiber followed by the coherence isomorphisms coming from F.
Русский
У заданного подъёма φ′ над g ∘ f из a′ в ⟨S, a⟩ существует каноническое отображение из a′ в область-Картезианского подъёма domainCartesianLift(a, f) с основанием g и волоковой (ферезной) частью, полученной из φ′ путём композиции с соответствующими изоморфизмами, исходящими из псефунктора F.
LaTeX
$$$\\text{homCartesianLift}(f,g,\\phi') : a' \\to \\operatorname{domainCartesianLift}(a,f)$$$
Lean4
/-- Given some lift `φ'` of `g ≫ f`, the canonical map from the domain of `φ'` to the domain of
the Cartesian lift of `f`. -/
abbrev homCartesianLift {a' : ∫ᶜ F} (g : a'.1 ⟶ R) (φ' : a' ⟶ ⟨S, a⟩) [IsHomLift (forget F) (g ≫ f) φ'] :
a' ⟶ domainCartesianLift a f where
base := g
fiber :=
have : φ'.base = g ≫ f := by simpa using IsHomLift.fac' (forget F) (g ≫ f) φ'
φ'.fiber ≫ eqToHom (by simp [this]) ≫ (F.mapComp f.op.toLoc g.op.toLoc).hom.app a
