English
For a evenly covered structure, the trivialization at x maps the chosen fiber element to (x, the corresponding coordinate). In particular, the second coordinate equals ⟨x, rfl⟩.
Русский
Для равномерного покрытия тривиализация в x отправляет выбранный элемент волокна в (x, соответствующая координата). В частности, вторая координата равна ⟨x, rfl⟩.
LaTeX
$$$(h.toTrivialization\\ x).2 = \\langle x, rfl \\rangle$$$
Lean4
/-- If `x : X` is evenly covered by `f` with fiber `I`, then `I` is homeomorphic to `f ⁻¹' {x}`. -/
noncomputable def fiberHomeomorph {x : X} (h : IsEvenlyCovered f x I) : I ≃ₜ f ⁻¹' { x } :=
by
choose _ U hxU hU hfU H hH using h
exact
{ toFun i := ⟨H.symm (⟨x, hxU⟩, i), by simp [← hH]⟩
invFun e := (H ⟨e, by rwa [Set.mem_preimage, (e.2 : f e = x)]⟩).2
left_inv _ := by simp
right_inv
e :=
Set.inclusion_injective (Set.preimage_mono (Set.singleton_subset_iff.mpr hxU)) <|
H.injective <| Prod.ext (Subtype.ext <| by simpa [hH] using e.2.symm) (by simp)
continuous_toFun := by fun_prop
continuous_invFun := by fun_prop }
