[Merged by Bors] - feat (LinearAlgebra/RootSystem/Finite): nondegeneracy of canonical bilinear form restricted to root span

[ScottCarnahan]

The canonical bilinear form for a root pairing over a linearly ordered commutative ring is nondegenerate when restricted to the span of roots.

---

[github-actions]

PR summary 4c23080813

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate	1393

---

Declarations diff

+ LinearMap.finrank_le_of_smul_regular
+ Submodule.disjoint_ker_of_finrank_eq
+ _root_.RootSystem.rootForm_anisotropic
+ corootSpan
+ disjoint_rootSpan_ker_polarization
+ eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero
+ finrank_corootSpan_eq
+ finrank_rootSpan_map_polarization_eq_finrank_corootSpan
+ instance : Module.Finite R P.corootSpan := Finite.span_of_finite R <| finite_range P.coroot
+ instance : Module.Finite R P.rootSpan := Finite.span_of_finite R <| finite_range P.root
+ instance [IsDomain R] : NoZeroSMulDivisors R M := by
+ mem_ker_polarization_of_rootForm_self_eq_zero
+ prod_rootForm_root_self_pos
+ prod_rootForm_smul_coroot_mem_range_domRestrict
+ range_polarization_domRestrict_le_span_coroot
+ rank_le_of_smul_regular
+ rootForm_pos_of_nonzero
+ rootForm_restrict_nondegenerate
+ rootForm_rootPositive
+ rootForm_root_self_pos
+ rootForm_self_non_neg
+ rootForm_self_zero_iff
+ rootSpan
+ sum_mul_self_eq_zero_iff

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[ocfnash]

Very nice!

I've just done a first pass. However I can't help wondering if you really need to be working with both Module.rank and Module.finrank. Would it be possible to avoid Module.rank and just use Module.finrank throughout?

[ocfnash]

Possible approach for the contents of Nondegenerate.lean which I think should work well:

section GeneralScalarsMoveToDefs

abbrev rootSpan := span R (range P.root)

abbrev corootSpan := span R (range P.coroot)

instance : Module.Finite R P.rootSpan := Finite.span_of_finite R <| finite_range P.root

instance : Module.Finite R P.corootSpan := Finite.span_of_finite R <| finite_range P.coroot

end GeneralScalarsMoveToDefs

@[simp]
lemma finrank_rootSpan_map_polarization_eq_finrank_corootSpan :
    finrank R (P.rootSpan.map P.Polarization) = finrank R P.corootSpan := by
  sorry

@[simp]
lemma finrank_corootSpan_map_coPolarization_eq_finrank_crootSpan :
    finrank R (P.corootSpan.map P.CoPolarization) = finrank R P.rootSpan :=
  P.flip.finrank_rootSpan_map_polarization_eq_finrank_corootSpan

/-- An auxiliary lemma en route to `RootPairing.finrank_corootSpan_eq`. -/
private lemma finrank_corootSpan_le :
    finrank R P.corootSpan ≤ finrank R P.rootSpan := by
  sorry

lemma finrank_corootSpan_eq :
    finrank R P.corootSpan = finrank R P.rootSpan :=
  le_antisymm P.finrank_corootSpan_le P.flip.finrank_corootSpan_le

lemma disjoint_rootSpan_ker_polarization :
    Disjoint P.rootSpan (LinearMap.ker P.Polarization) := by
  sorry

lemma mem_ker_polarization_of_rootForm_self_eq_zero {x : M} (hx : P.RootForm x x = 0) :
    x ∈ LinearMap.ker P.Polarization := by
  rw [LinearMap.mem_ker, Polarization_apply]
  rw [rootForm_self_zero_iff] at hx
  exact Fintype.sum_eq_zero _ fun i ↦ by simp [hx i]

lemma eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero {x : M}
    (hx : x ∈ P.rootSpan) (hx' : P.RootForm x x = 0) :
    x = 0 := by
  rw [← Submodule.mem_bot (R := R), ← P.disjoint_rootSpan_ker_polarization.eq_bot]
  exact ⟨hx, P.mem_ker_polarization_of_rootForm_self_eq_zero hx'⟩

-- Requires adding `import Mathlib.LinearAlgebra.QuadraticForm.Basic`
lemma _root_.RootSystem.rootFormAnisotropic (P : RootSystem ι R M N) :
    P.RootForm.toQuadraticMap.Anisotropic := by
  refine fun x ↦ P.eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero ?_
  rw [rootSpan, P.span_eq_top]
  exact Submodule.mem_top

[jcommelin]

I will try to review more later

[ScottCarnahan]

bot fix style

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style

[vihdzp]

This can be proven in greater generality and much more easily:

theorem sum_mul_self_eq_zero_iff [LinearOrderedRing R] (s : Finset ι) (f : ι → R) :
    ∑ i ∈ s, f i * f i = 0 ↔ ∀ i ∈ s, f i = 0 := by
  rw [sum_eq_zero_iff_of_nonneg fun _ _ ↦ mul_self_nonneg _]
  simp

I do this golfing in my own inequality PR #19311.

[ScottCarnahan]

That is much better!