English
Inclusion from a fiber of a composition into the intermediate fiber is given by projecting to the first component.
Русский
Включение из волокна композиции в промежуточное волокно задаётся проекцией на первую компоненту.
LaTeX
$$$$\sigma\text{InclIncl}_{f,g}(a) :(b\mapsto b.\mathrm{val})$$$$
Lean4
/-- The inclusion map from a fiber of a composition into the intermediate fiber. -/
def sigmaInclIncl {X : Type*} (g : Y → X) (a : Fiber (g ∘ f)) (b : Fiber (f ∘ (sigmaIncl (g ∘ f) a))) :
C(b.val, (Fiber.mk f (b.preimage).val).val) where
toFun
x :=
⟨x.val.val, by
have := x.prop
simp only [sigmaIncl, ContinuousMap.coe_mk, Fiber.mem_iff_eq_image, comp_apply] at this
rw [Fiber.mem_iff_eq_image, Fiber.mk_image, this, ← Fiber.map_preimage_eq_image]
simp [sigmaIncl]⟩
