fiberHomeo — Mathlib

English

The underlying map of the fiberHomeo between the fiber and its preimage coincides with the base-fiber map.

Русский

Базовая карта между волокном и его предобразом совпадает с базовой связью волокна и фундаментального отображения.

LaTeX

$$(f.fiberHomeo y)(x).1 = (f.fiberι y).base x$$

Lean4

/-- The scheme-theoretic fiber of `f` at `y` is homeomorphic to `f ⁻¹' {y}`. -/
def fiberHomeo (f : X.Hom Y) (y : Y) : f.fiber y ≃ₜ f.base ⁻¹' { y } :=
  .trans (f.fiberι y).isEmbedding.toHomeomorph (.setCongr (f.range_fiberι y))

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