incl_comap — Mathlib

English

This auxiliary map gives a morphism between fibers induced by a fiber element a, namely a map from fiber r a to Y at fiber r a.

Русский

Вспомогательная карта задаёт морфизм между фибрами, индуцированный элементом a, т. е. отображение из fiber r a в Y на fiber r a.

LaTeX

$$$\text{componentHom}(a) : \mathrm{fiber}\; r\; a \to \mathrm{fiber}\; r\; (Fiber.mk\, r\, a)$$$

Lean4

theorem incl_comap {S T : (CompHausLike P)ᵒᵖ}
    (f : LocallyConstant S.unop (Y.obj (op (CompHausLike.of P PUnit.{u + 1})))) (g : S ⟶ T)
    (a : Fiber (f.comap g.unop.hom)) :
    g ≫ (sigmaIncl (f.comap g.unop.hom) a).op = (sigmaIncl f _).op ≫ (componentHom f g.unop a).op :=
  rfl

Похожие утверждения