English
A variant of the previous lemma: under CharZero and NoZeroSMulDivisors, with Φ finite, if x belongs to span Φ, and hf₁, hf₂, hg₁, hg₂ satisfy the preReflection mapsTo conditions, then the equalities of dual maps hold at the span projection.
Русский
Вариант предыдущего леммы: при CharZero и NoZeroSMulDivisors, Φ конечен, если x ∈ span Φ и hf₁, hf₂, hg₁, hg₂ удовлетворяют условиям MapsTo для префReflection, то двойственные отображения совпадают на соответствующей проекции span.
LaTeX
$$$[CharZero\\ R][NoZeroSMulDivisors\\ R\\ M]\\ {x:\\ M}\\ {\\Phi:\\ Set M} (hΦ₁ : Φ.Finite) (hx : x ∈ span R Φ) {f g : Dual R M} (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
/-- This rather technical-looking lemma exists because it is exactly what is needed to establish a
uniqueness result for root data. See the doc string of `Module.Dual.eq_of_preReflection_mapsTo` for
further remarks. -/
theorem eq_of_preReflection_mapsTo' [CharZero R] [NoZeroSMulDivisors R M] {x : M} {Φ : Set M} (hΦ₁ : Φ.Finite)
(hx : x ∈ span R Φ) {f g : Dual R M} (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 :=
by
set Φ' : Set (span R Φ) := range (inclusion <| Submodule.subset_span (R := R) (s := Φ))
rw [← finite_coe_iff] at hΦ₁
have hΦ'₁ : Φ'.Finite := finite_range (inclusion Submodule.subset_span)
have hΦ'₂ : span R Φ' = ⊤ := by
simp only [Φ']
rw [range_inclusion]
simp
let x' : span R Φ := ⟨x, hx⟩
have this :
∀ {F : Dual R M}, MapsTo (preReflection x F) Φ Φ → MapsTo (preReflection x' ((span R Φ).subtype.dualMap F)) Φ' Φ' :=
by
intro F hF ⟨y, hy⟩ hy'
simp only [Φ'] at hy' ⊢
rw [range_inclusion] at hy'
simp only [SetLike.coe_sort_coe, mem_setOf_eq] at hy' ⊢
rw [range_inclusion]
exact hF hy'
exact eq_of_preReflection_mapsTo hΦ'₁ hΦ'₂ hf₁ (this hf₂) hg₁ (this hg₂)
