structure
ChevalleyRestrictionData
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
(wg : WeylGroupData Δ)
:
Type (max (max (max u_1 u_2) (u_3 + 1)) u_4)
- S𝔤 : Type u_3
- adInvariant : Subalgebra R self.S𝔤
- restriction_equivariant (w : wg.W) (f : self.S𝔤) : self.restrictionAlgHom ((self.algActionOnS𝔤 w) f) = (wg.algAction w) (self.restrictionAlgHom f)
- eval𝔤 : self.S𝔤 → 𝔤 → R
- eval𝔥 : UniversalEnvelopingAlgebra R ↥Δ.𝔥 → ↥Δ.𝔥 → R
- eval𝔤_injective : Function.Injective self.eval𝔤
- eval𝔥_injective : Function.Injective self.eval𝔥
- trace_function_surjectivity (p : UniversalEnvelopingAlgebra R ↥Δ.𝔥) : p ∈ wg.invariantSubalgebra → ∃ f ∈ self.adInvariant, ∀ (h : ↥Δ.𝔥), self.eval𝔥 (self.restrictionAlgHom f) h = self.eval𝔥 p h
Instances For
noncomputable def
killingFormDualIso
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
[LieAlgebra.IsKilling R 𝔤]
[FiniteDimensional R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
:
Instances For
noncomputable def
TriangularDecomposition.projectToH
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
(x : 𝔤)
:
↥Δ.𝔥
Instances For
theorem
TriangularDecomposition.projectToH_of_mem_h
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
(h : ↥Δ.𝔥)
:
noncomputable def
chevalleyEval𝔥
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
[LieAlgebra.IsKilling R 𝔤]
[FiniteDimensional R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
(p : UniversalEnvelopingAlgebra R ↥Δ.𝔥)
(h : ↥Δ.𝔥)
:
R
Instances For
noncomputable def
chevalleyEval𝔤
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
[LieAlgebra.IsKilling R 𝔤]
[FiniteDimensional R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
(f : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)))
(x : 𝔤)
:
R
Instances For
noncomputable def
chevalleyRestrictionData
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
[LieAlgebra.IsKilling R 𝔤]
[FiniteDimensional R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
(wg : WeylGroupData Δ)
:
Instances For
theorem
chevalley_restriction_lands_in_W_invariants_aux
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
(crd : ChevalleyRestrictionData Δ wg)
(f : crd.S𝔤)
(hf : f ∈ crd.adInvariant)
:
def
ChevalleyRestrictionData.restrictionMap
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
(crd : ChevalleyRestrictionData Δ wg)
:
Instances For
theorem
chevalley_restriction_injective_aux
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
(crd : ChevalleyRestrictionData Δ wg)
:
theorem
chevalley_restriction_surjective_aux
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
(crd : ChevalleyRestrictionData Δ wg)
:
theorem
chevalley_restriction_bijective_aux
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
(crd : ChevalleyRestrictionData Δ wg)
:
theorem
chevalley_restriction_lands_in_W_invariants
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
[LieAlgebra.IsKilling R 𝔤]
[FiniteDimensional R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
(f : (chevalleyRestrictionData wg).S𝔤)
(hf : f ∈ (chevalleyRestrictionData wg).adInvariant)
:
theorem
chevalley_restriction_injective
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
[LieAlgebra.IsKilling R 𝔤]
[FiniteDimensional R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
:
theorem
chevalley_restriction_surjective
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
[LieAlgebra.IsKilling R 𝔤]
[FiniteDimensional R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
:
theorem
chevalley_restriction_bijective
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
[LieAlgebra.IsKilling R 𝔤]
[FiniteDimensional R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
:
noncomputable def
chevalleyRestrictionAlgEquiv
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
[LieAlgebra.IsKilling R 𝔤]
[FiniteDimensional R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
:
Instances For
structure
IsComplexReflection
{k : Type u_3}
[Field k]
{V : Type u_4}
[AddCommGroup V]
[Module k V]
(g : V ≃ₗ[k] V)
:
Instances For
theorem
isComplexReflection_inv
{k : Type u_3}
[Field k]
{V : Type u_4}
[AddCommGroup V]
[Module k V]
(g : V ≃ₗ[k] V)
(h : IsComplexReflection g)
:
theorem
isComplexReflectionGroup_of_closure_eq_top
{k : Type u_3}
[Field k]
{V : Type u_4}
[AddCommGroup V]
[Module k V]
{G : Type u_5}
[Group G]
[Fintype G]
(ρ : G →* V ≃ₗ[k] V)
(hclosure : Subgroup.closure {g : G | IsComplexReflection (ρ g)} = ⊤)
:
noncomputable def
polynomialInvariantSubalgebra
(k : Type u_3)
[CommSemiring k]
(G : Type u_4)
[Group G]
(ι : Type u_5)
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
:
Subalgebra k (MvPolynomial ι k)
Instances For
def
IsInducedPolynomialAction
{k : Type u_3}
[CommRing k]
{V : Type u_4}
[AddCommGroup V]
[Module k V]
{ι : Type u_5}
[Fintype ι]
[DecidableEq ι]
(b : Module.Basis ι k V)
(G : Type u_6)
[Group G]
(ρ : G →* V ≃ₗ[k] V)
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
:
Instances For
Instances For
theorem
noether_lemma11_1_finite_generation
{k : Type u_3}
[Field k]
[CharZero k]
{G : Type u_4}
[Group G]
[Fintype G]
{ι : Type u_5}
[Fintype ι]
[DecidableEq ι]
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
(h_deg_pres : ∀ (g : G) (p : MvPolynomial ι k), ((algAct g) p).totalDegree ≤ p.totalDegree)
:
∃ (r : ℕ) (f : Fin r → MvPolynomial ι k),
(∀ (i : Fin r), f i ∈ polynomialInvariantSubalgebra k G ι algAct) ∧ polynomialInvariantSubalgebra k G ι algAct = Algebra.adjoin k (Set.range f)
theorem
lemma_11_4_algebraic_independence_upgrade
{k : Type u_3}
[Field k]
[CharZero k]
[IsAlgClosed k]
{V : Type u_4}
[AddCommGroup V]
[Module k V]
[Module.Finite k V]
(G : Type u_5)
[Group G]
[Fintype G]
(ρ : G →* V ≃ₗ[k] V)
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
(b : Module.Basis ι k V)
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
(hcompat : IsInducedPolynomialAction b G ρ algAct)
(hG : IsComplexReflectionGroup G ρ)
(r : ℕ)
(f : Fin r → MvPolynomial ι k)
(hf_inv : ∀ (i : Fin r), f i ∈ polynomialInvariantSubalgebra k G ι algAct)
(hf_gen : polynomialInvariantSubalgebra k G ι algAct = Algebra.adjoin k (Set.range f))
:
∃ (s : ℕ) (g : Fin s → MvPolynomial ι k),
(∀ (i : Fin s), g i ∈ polynomialInvariantSubalgebra k G ι algAct) ∧ AlgebraicIndependent k g ∧ polynomialInvariantSubalgebra k G ι algAct = Algebra.adjoin k (Set.range g)
theorem
isInducedPolynomialAction_deg_pres
{k : Type u_3}
[Field k]
{V : Type u_4}
[AddCommGroup V]
[Module k V]
{G : Type u_5}
[Group G]
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
(b : Module.Basis ι k V)
(ρ : G →* V ≃ₗ[k] V)
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
(hcompat : IsInducedPolynomialAction b G ρ algAct)
(g : G)
(p : MvPolynomial ι k)
:
theorem
hilbert_lemma11_1_lemma11_4_combined
{k : Type u_3}
[Field k]
[CharZero k]
[IsAlgClosed k]
{V : Type u_4}
[AddCommGroup V]
[Module k V]
[Module.Finite k V]
(G : Type u_5)
[Group G]
[Fintype G]
(ρ : G →* V ≃ₗ[k] V)
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
(b : Module.Basis ι k V)
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
(hcompat : IsInducedPolynomialAction b G ρ algAct)
(hG : IsComplexReflectionGroup G ρ)
:
∃ (r : ℕ) (f : Fin r → MvPolynomial ι k),
(∀ (i : Fin r), f i ∈ polynomialInvariantSubalgebra k G ι algAct) ∧ AlgebraicIndependent k f ∧ polynomialInvariantSubalgebra k G ι algAct = Algebra.adjoin k (Set.range f)
noncomputable def
orbitPoly
{k : Type u_3}
[Field k]
{G : Type u_4}
[Group G]
[Fintype G]
{ι : Type u_5}
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
(p : MvPolynomial ι k)
:
Polynomial (MvPolynomial ι k)
Instances For
theorem
orbitPoly_monic
{k : Type u_3}
[Field k]
{G : Type u_4}
[Group G]
[Fintype G]
{ι : Type u_5}
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
(p : MvPolynomial ι k)
:
theorem
orbitPoly_eval
{k : Type u_3}
[Field k]
{G : Type u_4}
[Group G]
[Fintype G]
{ι : Type u_5}
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
(p : MvPolynomial ι k)
:
theorem
orbitPoly_map_invariant
{k : Type u_3}
[Field k]
{G : Type u_4}
[Group G]
[Fintype G]
[DecidableEq G]
{ι : Type u_5}
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
(p : MvPolynomial ι k)
(h : G)
:
theorem
orbitPoly_coeff_mem
{k : Type u_3}
[Field k]
{G : Type u_4}
[Group G]
[Fintype G]
[DecidableEq G]
{ι : Type u_5}
[Fintype ι]
[DecidableEq ι]
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
(p : MvPolynomial ι k)
(n : ℕ)
:
theorem
orbitPoly_coeffs_subset
{k : Type u_3}
[Field k]
{G : Type u_4}
[Group G]
[Fintype G]
[DecidableEq G]
{ι : Type u_5}
[Fintype ι]
[DecidableEq ι]
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
(p : MvPolynomial ι k)
:
theorem
isIntegral_over_invariantSubalgebra
{k : Type u_3}
[Field k]
[CharZero k]
{G : Type u_4}
[Group G]
[Fintype G]
[DecidableEq G]
{ι : Type u_5}
[Fintype ι]
[DecidableEq ι]
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
(p : MvPolynomial ι k)
:
IsIntegral (↥(polynomialInvariantSubalgebra k G ι algAct)) p
theorem
remark_11_5_generators_eq_dim
{k : Type u_3}
[Field k]
[CharZero k]
[IsAlgClosed k]
(G : Type u_4)
[Group G]
[Fintype G]
{ι : Type u_5}
[Fintype ι]
[DecidableEq ι]
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
(r : ℕ)
(f : Fin r → MvPolynomial ι k)
(_hf_inv : ∀ (i : Fin r), f i ∈ polynomialInvariantSubalgebra k G ι algAct)
(hf_alg : AlgebraicIndependent k f)
(hf_gen : polynomialInvariantSubalgebra k G ι algAct = Algebra.adjoin k (Set.range f))
:
theorem
section11_algebraically_independent_generators
{k : Type u_3}
[Field k]
[CharZero k]
[IsAlgClosed k]
{V : Type u_4}
[AddCommGroup V]
[Module k V]
[Module.Finite k V]
(G : Type u_5)
[Group G]
[Fintype G]
(ρ : G →* V ≃ₗ[k] V)
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
(b : Module.Basis ι k V)
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
(hcompat : IsInducedPolynomialAction b G ρ algAct)
(hG : IsComplexReflectionGroup G ρ)
:
∃ (f : Fin (Fintype.card ι) → MvPolynomial ι k),
(∀ (i : Fin (Fintype.card ι)), f i ∈ polynomialInvariantSubalgebra k G ι algAct) ∧ AlgebraicIndependent k f ∧ polynomialInvariantSubalgebra k G ι algAct = Algebra.adjoin k (Set.range f)
theorem
chevalley_shephard_todd_forward
{k : Type u_3}
[Field k]
[CharZero k]
[IsAlgClosed k]
{V : Type u_4}
[AddCommGroup V]
[Module k V]
[Module.Finite k V]
(G : Type u_5)
[Group G]
[Fintype G]
(ρ : G →* V ≃ₗ[k] V)
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
(b : Module.Basis ι k V)
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
(hcompat : IsInducedPolynomialAction b G ρ algAct)
(hG : IsComplexReflectionGroup G ρ)
:
IsPolynomialAlgebra ↥(polynomialInvariantSubalgebra k G ι algAct)
theorem
reflection_subgroup_is_reflection_group
{k : Type u_3}
[Field k]
{V : Type u_4}
[AddCommGroup V]
[Module k V]
{G : Type u_5}
[Group G]
[Fintype G]
(ρ : G →* V ≃ₗ[k] V)
(H : Subgroup G)
[Fintype ↥H]
(hH : H = Subgroup.closure {g : G | IsComplexReflection (ρ g)})
:
IsComplexReflectionGroup (↥H) (ρ.comp H.subtype)
theorem
isInducedPolynomialAction_restrict
{k : Type u_3}
[CommRing k]
{V : Type u_4}
[AddCommGroup V]
[Module k V]
{ι : Type u_5}
[Fintype ι]
[DecidableEq ι]
(b : Module.Basis ι k V)
{G : Type u_6}
[Group G]
(ρ : G →* V ≃ₗ[k] V)
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
(hcompat : IsInducedPolynomialAction b G ρ algAct)
(H : Subgroup G)
:
IsInducedPolynomialAction b (↥H) (ρ.comp H.subtype) (algAct.comp H.subtype)
theorem
jacobian_argument_invariants_eq
{k : Type u_3}
[Field k]
[CharZero k]
[IsAlgClosed k]
{V : Type u_4}
[AddCommGroup V]
[Module k V]
[Module.Finite k V]
(G : Type u_5)
[Group G]
[Fintype G]
(ρ : G →* V ≃ₗ[k] V)
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
(b : Module.Basis ι k V)
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
(hcompat : IsInducedPolynomialAction b G ρ algAct)
(hpoly_G : IsPolynomialAlgebra ↥(polynomialInvariantSubalgebra k G ι algAct))
(H : Subgroup G)
(hH : H = Subgroup.closure {g : G | IsComplexReflection (ρ g)})
(hpoly_H : IsPolynomialAlgebra ↥(polynomialInvariantSubalgebra k (↥H) ι (algAct.comp H.subtype)))
:
theorem
reflections_generate_of_polynomial_invariants
{k : Type u_3}
[Field k]
[CharZero k]
[IsAlgClosed k]
{V : Type u_4}
[AddCommGroup V]
[Module k V]
[Module.Finite k V]
(G : Type u_5)
[Group G]
[Fintype G]
(ρ : G →* V ≃ₗ[k] V)
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
(b : Module.Basis ι k V)
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
(hcompat : IsInducedPolynomialAction b G ρ algAct)
(hpoly : IsPolynomialAlgebra ↥(polynomialInvariantSubalgebra k G ι algAct))
:
theorem
chevalley_shephard_todd_reverse
{k : Type u_3}
[Field k]
[CharZero k]
[IsAlgClosed k]
{V : Type u_4}
[AddCommGroup V]
[Module k V]
[Module.Finite k V]
(G : Type u_5)
[Group G]
[Fintype G]
(ρ : G →* V ≃ₗ[k] V)
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
(b : Module.Basis ι k V)
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
(hcompat : IsInducedPolynomialAction b G ρ algAct)
(hpoly : IsPolynomialAlgebra ↥(polynomialInvariantSubalgebra k G ι algAct))
:
theorem
chevalley_shephard_todd_iff
{k : Type u_3}
[Field k]
[CharZero k]
[IsAlgClosed k]
{V : Type u_4}
[AddCommGroup V]
[Module k V]
[Module.Finite k V]
(G : Type u_5)
[Group G]
[Fintype G]
(ρ : G →* V ≃ₗ[k] V)
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
(b : Module.Basis ι k V)
(algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k)
(hcompat : IsInducedPolynomialAction b G ρ algAct)
:
theorem
weyl_group_invariants_is_polynomial_algebra
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
[LieAlgebra.IsKilling R 𝔤]
[FiniteDimensional R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
(wg : WeylGroupData Δ)
:
structure
ChevalleyRestrictionPolyData
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
(wg : WeylGroupData Δ)
(n m : ℕ)
:
Type (max (max u_1 (u_3 + 1)) u_4)
- G : Type u_3
- Res_components : Fin n → MvPolynomial (Fin m) R
- Res_components_homogeneous (i : Fin n) : (self.Res_components i).IsHomogeneous 1
- kernel_trivial (p : MvPolynomial (Fin n) R) : p ∈ Subalgebra.invariants self.G self.G_action → self.Res p = 0 → p = 0
Instances For
theorem
ChevalleyRestrictionPolyData.Res_preserves_degree
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
{n m : ℕ}
(cpd : ChevalleyRestrictionPolyData wg n m)
(p : MvPolynomial (Fin n) R)
(d : ℕ)
(hp : p.IsHomogeneous d)
:
(cpd.Res p).IsHomogeneous d
theorem
ChevalleyRestrictionPolyData.Res_maps_invariants
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
{n m : ℕ}
(cpd : ChevalleyRestrictionPolyData wg n m)
(p : MvPolynomial (Fin n) R)
(hp : p ∈ Subalgebra.invariants cpd.G cpd.G_action)
:
theorem
semisimple_conjugate_to_cartan
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
{n m : ℕ}
(cpd : ChevalleyRestrictionPolyData wg n m)
(S : Set (Fin n → R))
(v : Fin n → R)
:
v ∈ S →
∀ p ∈ Subalgebra.invariants cpd.G cpd.G_action,
∃ (h : Fin m → R), (MvPolynomial.eval v) p = (MvPolynomial.eval h) (cpd.Res p)
theorem
semisimple_elements_zariski_dense
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
{n m : ℕ}
(cpd : ChevalleyRestrictionPolyData wg n m)
(S : Set (Fin n → R))
(p : MvPolynomial (Fin n) R)
(hvanish : ∀ v ∈ S, (MvPolynomial.eval v) p = 0)
:
theorem
invariant_vanishes_on_semisimple_locus
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
{n m : ℕ}
(cpd : ChevalleyRestrictionPolyData wg n m)
(S : Set (Fin n → R))
(hconj :
∀ v ∈ S,
∀ p ∈ Subalgebra.invariants cpd.G cpd.G_action,
∃ (h : Fin m → R), (MvPolynomial.eval v) p = (MvPolynomial.eval h) (cpd.Res p))
(p : MvPolynomial (Fin n) R)
(hp : p ∈ Subalgebra.invariants cpd.G cpd.G_action)
(hker : cpd.Res p = 0)
(v : Fin n → R)
:
v ∈ S → (MvPolynomial.eval v) p = 0
theorem
semisimple_zariski_density_injectivity
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
{n m : ℕ}
(cpd : ChevalleyRestrictionPolyData wg n m)
(p : MvPolynomial (Fin n) R)
(hp : p ∈ Subalgebra.invariants cpd.G cpd.G_action)
(hker : cpd.Res p = 0)
:
theorem
trace_functions_span_W_invariants
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
{n m : ℕ}
(cpd : ChevalleyRestrictionPolyData wg n m)
:
∃ (Λ : Type) (F : Λ → MvPolynomial (Fin n) R),
(∀ (l : Λ), F l ∈ Subalgebra.invariants cpd.G cpd.G_action) ∧ ∀ q ∈ Subalgebra.invariants wg.W cpd.W_action, q ∈ Algebra.adjoin R (Set.range (⇑cpd.Res ∘ F))
theorem
ChevalleyRestrictionPolyData.Res_surjective'
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
{n m : ℕ}
(cpd : ChevalleyRestrictionPolyData wg n m)
(q : MvPolynomial (Fin m) R)
(hq : q ∈ Subalgebra.invariants wg.W cpd.W_action)
:
∃ p ∈ Subalgebra.invariants cpd.G cpd.G_action, cpd.Res p = q
noncomputable def
ChevalleyRestrictionPolyData.restrictionMapPoly
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
{n m : ℕ}
(cpd : ChevalleyRestrictionPolyData wg n m)
:
Instances For
theorem
chevalley_restriction_polynomial
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
{n m : ℕ}
(cpd : ChevalleyRestrictionPolyData wg n m)
:
noncomputable def
chevalleyRestrictionPolynomialAlgEquiv
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
{n m : ℕ}
(cpd : ChevalleyRestrictionPolyData wg n m)
:
Instances For
theorem
chevalley_res_kernel_trivial_on_invariants
{k : Type u_3}
[CommRing k]
{n m : ℕ}
(G : Type u_4)
[Group G]
(G_action : G →* MvPolynomial (Fin n) k ≃ₐ[k] MvPolynomial (Fin n) k)
(Res : MvPolynomial (Fin n) k →ₐ[k] MvPolynomial (Fin m) k)
(hRes_kernel_trivial : ∀ q ∈ Subalgebra.invariants G G_action, Res q = 0 → q = 0)
(p : MvPolynomial (Fin n) k)
(hp_inv : p ∈ Subalgebra.invariants G G_action)
(hp_ker : Res p = 0)
:
theorem
chevalley_res_injective_on_invariants
{k : Type u_3}
[CommRing k]
{n m : ℕ}
(G : Type u_4)
[Group G]
(G_action : G →* MvPolynomial (Fin n) k ≃ₐ[k] MvPolynomial (Fin n) k)
(Res : MvPolynomial (Fin n) k →ₐ[k] MvPolynomial (Fin m) k)
(hRes_kernel_trivial : ∀ q ∈ Subalgebra.invariants G G_action, Res q = 0 → q = 0)
(p₁ p₂ : MvPolynomial (Fin n) k)
(hp₁ : p₁ ∈ Subalgebra.invariants G G_action)
(hp₂ : p₂ ∈ Subalgebra.invariants G G_action)
(h : Res p₁ = Res p₂)
:
theorem
chevalley_res_surjective_on_invariants
{k : Type u_3}
[Field k]
{𝔤₀ : Type u_4}
[LieRing 𝔤₀]
[LieAlgebra k 𝔤₀]
[LieAlgebra.IsKilling k 𝔤₀]
[FiniteDimensional k 𝔤₀]
{Δ : TriangularDecomposition k 𝔤₀}
{wg : WeylGroupData Δ}
{n m : ℕ}
(cpd : ChevalleyRestrictionPolyData wg n m)
(q : MvPolynomial (Fin m) k)
(hq : q ∈ Subalgebra.invariants wg.W cpd.W_action)
:
∃ p ∈ Subalgebra.invariants cpd.G cpd.G_action, cpd.Res p = q
theorem
chevalley_restriction_theorem_10_1
{k : Type u_3}
[Field k]
{𝔤₀ : Type u_4}
[LieRing 𝔤₀]
[LieAlgebra k 𝔤₀]
[LieAlgebra.IsKilling k 𝔤₀]
[FiniteDimensional k 𝔤₀]
{Δ : TriangularDecomposition k 𝔤₀}
{wg : WeylGroupData Δ}
{n m : ℕ}
(cpd : ChevalleyRestrictionPolyData wg n m)
:
Function.Bijective
⇑((cpd.Res.comp (Subalgebra.invariants cpd.G cpd.G_action).val).codRestrict (Subalgebra.invariants wg.W cpd.W_action)
⋯)
noncomputable def
chevalleyRestrictionTheorem_10_1_algEquiv
{k : Type u_3}
[Field k]
{𝔤₀ : Type u_4}
[LieRing 𝔤₀]
[LieAlgebra k 𝔤₀]
[LieAlgebra.IsKilling k 𝔤₀]
[FiniteDimensional k 𝔤₀]
{Δ : TriangularDecomposition k 𝔤₀}
{wg : WeylGroupData Δ}
{n m : ℕ}
(cpd : ChevalleyRestrictionPolyData wg n m)
:
Instances For
noncomputable def
chevalley_restriction_isomorphism
{k : Type u_3}
[Field k]
{𝔤₀ : Type u_4}
[LieRing 𝔤₀]
[LieAlgebra k 𝔤₀]
[LieAlgebra.IsKilling k 𝔤₀]
[FiniteDimensional k 𝔤₀]
{Δ : TriangularDecomposition k 𝔤₀}
{wg : WeylGroupData Δ}
{n m : ℕ}
(cpd : ChevalleyRestrictionPolyData wg n m)
:
Instances For
theorem
chevalley_restriction_graded_isomorphism
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{wg : WeylGroupData Δ}
{n m : ℕ}
(cpd : ChevalleyRestrictionPolyData wg n m)
:
Function.Bijective ⇑cpd.restrictionMapPoly ∧ ∀ (p : MvPolynomial (Fin n) R) (d : ℕ), p.IsHomogeneous d → (cpd.Res p).IsHomogeneous d