eq_of_preReflection_mapsTo — Mathlib

English

Assume CharZero and NoZeroSMulDivisors; with finite Φ, f x = 2, MapsTo preReflection x f Φ Φ; g x = 2, MapsTo preReflection x g Φ Φ; then the restricted dual maps on span Φ coincide: (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g.

Русский

Пусть CharZero и NoZeroSMulDivisors; при конечном Φ, f x = 2, MapsTo preReflection x f Φ Φ; g x = 2, MapsTo preReflection x g Φ Φ; тогда ограниченные двойственные отображения совпадают: (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g.

LaTeX

$$$[CharZero\\ R]\\ [NoZeroSMulDivisors\\ R\\ M]\\ {\\Phi:\\ Set M},\\ hf: f x = 2,\\ hΦ: MapsTo(preReflection x f,Φ,Φ),\\ hg: g x = 2,\\ h' : MapsTo(preReflection x g,Φ,Φ)\\Rightarrow\\n (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g.$$$

Lean4

/-- See also `Module.Dual.eq_of_preReflection_mapsTo'` for a variant of this lemma which
applies when `Φ` does not span.

This rather technical-looking lemma exists because it is exactly what is needed to establish various
uniqueness results for root data / systems. One might regard this lemma as lying at the boundary of
linear algebra and combinatorics since the finiteness assumption is the key. -/
theorem eq_of_preReflection_mapsTo [CharZero R] [NoZeroSMulDivisors R M] {x : M} {Φ : Set M} (hΦ₁ : Φ.Finite)
    (hΦ₂ : 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) Φ Φ) : f = g :=
  by
  have hx : x ≠ 0 := by rintro rfl; simp at hf₁
  let u := reflection hg₁ * reflection hf₁
  have hu : u = LinearMap.id (R := R) (M := M) + (f - g).smulRight x :=
    by
    ext y
    simp only [u, reflection_apply, hg₁, two_smul, LinearEquiv.coe_toLinearMap_mul, LinearMap.id_coe,
      LinearEquiv.coe_coe, Module.End.mul_apply, LinearMap.add_apply, id_eq, LinearMap.coe_smulRight,
      LinearMap.sub_apply, map_sub, map_smul, sub_add_cancel_left, smul_neg, sub_neg_eq_add, sub_smul]
    abel
  replace hu : ∀ (n : ℕ), ↑(u ^ n) = LinearMap.id (R := R) (M := M) + (n : R) • (f - g).smulRight x :=
    by
    intro n
    induction n with
    | zero => simp
    | succ n
      ih =>
      have : ((f - g).smulRight x).comp ((n : R) • (f - g).smulRight x) = 0 := by ext; simp [hf₁, hg₁]
      rw [pow_succ', LinearEquiv.coe_toLinearMap_mul, ih, hu, add_mul, mul_add, mul_add]
      simp_rw [Module.End.mul_eq_comp, LinearMap.comp_id, LinearMap.id_comp, this, add_zero, add_assoc, Nat.cast_succ,
        add_smul, one_smul]
  suffices IsOfFinOrder u by
    obtain ⟨n, hn₀, hn₁⟩ := isOfFinOrder_iff_pow_eq_one.mp this
    replace hn₁ : (↑(u ^ n) : M →ₗ[R] M) = LinearMap.id := LinearEquiv.toLinearMap_inj.mpr hn₁
    simpa [hn₁, hn₀.ne', hx, sub_eq_zero] using hu n
  exact u.isOfFinOrder_of_finite_of_span_eq_top_of_mapsTo hΦ₁ hΦ₂ (hg₂.comp hf₂)

Похожие утверждения