English
The induced functor induced by comp_const F S is full; i.e., every morphism in the target fiber can be lifted to a morphism in the source fiber via the induced functor.
Русский
Индуцированный функтор, получаемый из comp_const F S, полно по отношению к гамме; то есть каждый морфизм в целевой волокне может быть поднят до морфизма в исходной волокне через индуцированный функтор.
LaTeX
$$$\\operatorname{Full}(\\operatorname{inducedFunctor}(\\mathrm{comp\\_const} F S))$$$
Lean4
noncomputable instance : (Fiber.inducedFunctor (comp_const F S)).Full where
map_surjective {X Y}
f :=
by
have hf : (fiberInclusion.map f).base = 𝟙 S := by
simpa using (IsHomLift.fac (forget F) (𝟙 S) (fiberInclusion.map f)).symm
use (fiberInclusion.map f).2 ≫ eqToHom (by simp [hf]) ≫ (F.mapId ⟨op S⟩).hom.app Y
ext <;> simp [hf]
