English
For a ring hom f: F → K and P,Q ∈ F^3, (f ∘ P) ≈ (f ∘ Q) iff P ≈ Q, provided W is nonsingular for P and Q.
Русский
Для гомоморфизма f: F → K и P,Q ∈ F^3 верно: (f ∘ P) эквивалентно (f ∘ Q) тогда и тогда, когда W неособая для P и Q.
LaTeX
$$$ f \\circ P \\approx f \\circ Q \\;\\iff\\; P \\approx Q $$$
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⟩
