Skip to content

[Merged by Bors] - feat(Algebra/Lie): use IsApply for Weight #42129

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
mcdoll wants to merge 3 commits into from
Closed

[Merged by Bors] - feat(Algebra/Lie): use IsApply for Weight #42129

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
243c230
weights
mcdoll Jul 27, 2026
b09b067
Merge branch 'master' into IsApplyLie
mcdoll Jul 27, 2026
34c11e4
fix
mcdoll Jul 27, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 5 additions & 4 deletions Mathlib/Algebra/Lie/Weights/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -238,10 +238,12 @@ instance [Subsingleton M] : IsEmpty (Weight R L M) :=
instance [Nontrivial (genWeightSpace M (0 : L → R))] : Zero (Weight R L M) :=
⟨0, fun e ↦ not_nontrivial (⊥ : LieSubmodule R L M) (e ▸ ‹_›)⟩

@[simp]
lemma coe_zero [Nontrivial (genWeightSpace M (0 : L → R))] : ((0 : Weight R L M) : L → R) = 0 := rfl
instance [Nontrivial (genWeightSpace M (0 : L → R))] : IsZeroApply (Weight R L M) L R where
zero_apply _ := rfl

@[deprecated (since := "2026-07-27")] alias coe_zero := FunLike.coe_zero

lemma zero_apply [Nontrivial (genWeightSpace M (0 : L → R))] (x) : (0 : Weight R L M) x = 0 := rfl
@[deprecated (since := "2026-07-27")] protected alias zero_apply := zero_apply

/-- The proposition that a weight of a Lie module is zero.

Expand All @@ -266,7 +268,6 @@ lemma isNonZero_iff_ne_zero [Nontrivial (genWeightSpace M (0 : L → R))] {χ :

noncomputable instance : DecidablePred (IsNonZero (R := R) (L := L) (M := M)) := Classical.decPred _

set_option backward.isDefEq.respectTransparency.types false in
Comment thread
grunweg marked this conversation as resolved.
variable (R L M) in
/-- The set of weights is equivalent to a subtype. -/
def equivSetOfPred : Weight R L M ≃ {χ : L → R | genWeightSpace M χ ≠ ⊥} where
Expand Down
12 changes: 6 additions & 6 deletions Mathlib/Algebra/Lie/Weights/RootSystem.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -187,7 +187,7 @@ lemma chainLength_neg :

@[simp]
lemma chainLength_zero [Nontrivial L] : chainLength 0 β = 0 := by
simp [← chainBotCoeff_add_chainTopCoeff]
simp [← chainBotCoeff_add_chainTopCoeff, FunLike.coe_zero]

/-- If `β - qα ... β ... β + rα` is the `α`-chain through `β`, then
`β (coroot α) = q - r`. In particular, it is an integer. -/
Expand Down Expand Up @@ -263,7 +263,7 @@ lemma chainTopCoeff_zero_right [Nontrivial L] (hα : α.IsNonZero) :
apply eq_of_le_of_not_lt
· rw [Nat.one_le_iff_ne_zero]
intro e
exact α.2 (by simpa [e, Weight.coe_zero] using!
exact α.2 (by simpa [e, FunLike.coe_zero] using!
genWeightSpace_chainTopCoeff_add_one_nsmul_add α (0 : Weight K H L) hα)
obtain ⟨x, hx, x_ne0⟩ := (chainTop α (0 : Weight K H L)).exists_ne_zero
obtain ⟨h, e, f, isSl2, he, hf⟩ := exists_isSl2Triple_of_weight_isNonZero hα
Expand All @@ -275,7 +275,7 @@ lemma chainTopCoeff_zero_right [Nontrivial L] (hα : α.IsNonZero) :
(toEnd K L L f ^ (chainTopCoeff α (0 : Weight K H L) + 1)) x := by
have : (toEnd K L L f ^ (chainTopCoeff α (0 : Weight K H L) + 1)) x ∈ rootSpace H (-α) := by
convert toEnd_pow_apply_mem hf hx (chainTopCoeff α (0 : Weight K H L) + 1)
rw [coe_chainTop', Weight.coe_zero, add_zero, succ_nsmul',
rw [coe_chainTop', FunLike.coe_zero, add_zero, succ_nsmul',
add_assoc, smul_neg, neg_add_cancel, add_zero]
simpa using! (finrank_eq_one_iff_of_nonzero' ⟨f, hf⟩ (by simpa using! isSl2.f_ne_zero)).mp
(finrank_rootSpace_eq_one _ hα.neg) ⟨_, this⟩
Expand All @@ -284,7 +284,7 @@ lemma chainTopCoeff_zero_right [Nontrivial L] (hα : α.IsNonZero) :
intro e
refine prim.pow_toEnd_f_ne_zero_of_eq_nat rfl ?_ hk.symm
have := (apply_coroot_eq_cast' α 0).symm
simp only [← @Nat.cast_two ℤ, ← Nat.cast_mul, Weight.zero_apply, Int.cast_eq_zero, sub_eq_zero,
simp only [← @Nat.cast_two ℤ, ← Nat.cast_mul, zero_apply, Int.cast_eq_zero, sub_eq_zero,
Nat.cast_inj] at this
rwa [this, Nat.succ_le_iff, two_mul, add_lt_add_iff_left]

Expand All @@ -299,7 +299,7 @@ lemma chainLength_zero_right [Nontrivial L] (hα : α.IsNonZero) : chainLength
lemma rootSpace_two_smul (hα : α.IsNonZero) : rootSpace H (2 • α) = ⊥ := by
cases subsingleton_or_nontrivial L
· exact IsEmpty.elim inferInstance α
simpa [chainTopCoeff_zero_right α hα] using
simpa [FunLike.coe_zero, chainTopCoeff_zero_right α hα] using
genWeightSpace_chainTopCoeff_add_one_nsmul_add α (0 : Weight K H L) hα

lemma rootSpace_one_div_two_smul (hα : α.IsNonZero) : rootSpace H ((2⁻¹ : K) • α) = ⊥ := by
Expand Down Expand Up @@ -328,7 +328,7 @@ lemma eq_neg_one_or_eq_zero_or_eq_one_of_eq_smul
mul_eq_mul_left_iff, OfNat.ofNat_ne_zero, or_false] at H
rw [← Int.cast_natCast, ← Int.cast_natCast (chainTopCoeff α β), ← Int.cast_sub] at H
have := (rootSpace_zsmul_add_ne_bot_iff_mem α 0 hα (n - chainTopCoeff α β)).mp
(by rw [← Int.cast_smul_eq_zsmul K, ← H, ← h, Weight.coe_zero, add_zero]; exact β.2)
(by rw [← Int.cast_smul_eq_zsmul K, ← H, ← h, FunLike.coe_zero, add_zero]; exact β.2)
rw [chainTopCoeff_zero_right α hα, chainBotCoeff_zero_right α hα, Nat.cast_one] at this
set k' : ℤ := n - chainTopCoeff α β
subst H
Expand Down
Loading