English
Nonsingularity lifts through the quotient orbit: W′.NonsingularLift of the lifted point equals W'.Nonsingular at the representative.
Русский
Несингулярность поднимается через тождество орбиты по отношению эквивалентности: несингулярность лифта в точке равна несингулярности в соответствующей точке.
LaTeX
$$$W'.NonsingularLift(\\overline{P}) \\iff W'.Nonsingular P$$$
Lean4
theorem comp_equiv_comp (f : F →+* K) {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) :
f ∘ P ≈ f ∘ Q ↔ P ≈ Q := by
refine ⟨fun h => ?_, fun h => ?_⟩
· by_cases hz : f (P z) = 0
·
exact
equiv_of_Z_eq_zero hP hQ ((map_eq_zero_iff f f.injective).mp hz) <|
(map_eq_zero_iff f f.injective).mp <| (Z_eq_zero_of_equiv h).mp hz
· refine
equiv_of_X_eq_of_Y_eq ((map_ne_zero_iff f f.injective).mp hz)
((map_ne_zero_iff f f.injective).mp <| hz.comp (Z_eq_zero_of_equiv h).mpr) ?_ ?_
all_goals apply f.injective; map_simp
exacts [X_eq_of_equiv h, Y_eq_of_equiv h]
· rcases h with ⟨u, rfl⟩
exact ⟨Units.map f u, (comp_smul ..).symm⟩
