English
A variant of the equality of dual maps when passing to span Φ, under CharZero and NoZeroSMulDivisors; if hf₁, hf₂, hg₁, hg₂ hold, then the restricted dual maps agree on span Φ.
Русский
Вариант равенства двойственных отображений при переходе к span Φ, при CharZero и NoZeroSMulDivisors; если выполняются hf₁, hf₂, hg₁, hg₂, то ограниченные двойственные отображения совпадают на span Φ.
LaTeX
$$$[CharZero\\ R][NoZeroSMulDivisors\\ R\\ M]\\ Φ.Finite →\\ Equations\\n(hΦ: Φ.Finite)\\,(hf₁: f x =2) (hf₂: MapsTo (preReflection x f) Φ Φ) (hg₁: g x =2) (hg₂: MapsTo (preReflection x g) Φ Φ) : (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g$$$
Lean4
theorem eq_of_mapsTo_reflection_of_mem [NoZeroSMulDivisors ℤ M] {Φ : Set M} (hΦ : Φ.Finite) (hfx : f x = 2)
(hgy : g y = 2) (hgx : g x = 2) (hfy : f y = 2) (hxfΦ : MapsTo (preReflection x f) Φ Φ)
(hygΦ : MapsTo (preReflection y g) Φ Φ) (hyΦ : y ∈ Φ) : x = y :=
by
suffices h : f y • x = (2 : R) • y
by
rw [hfy, two_smul R x, two_smul R y, ← two_zsmul, ← two_zsmul] at h
exact smul_right_injective _ two_ne_zero h
rw [← not_infinite] at hΦ
contrapose! hΦ
apply ((infinite_range_reflection_reflection_iterate_iff hfx hgy (by rw [hfy, hgx]; norm_cast)).mpr hΦ).mono
rw [range_subset_iff]
intro n
rw [←
IsFixedPt.image_iterate ((bijOn_reflection_of_mapsTo hfx hxfΦ).comp (bijOn_reflection_of_mapsTo hgy hygΦ)).image_eq
n]
exact mem_image_of_mem _ hyΦ
