noncomputable def qIntegerCST (d : ℕ) : PowerSeries ℤ

noncomputable def quotientGradedComponent (n : ℕ) (I : Ideal (MvPolynomial (Fin n) ℂ)) (N : ℕ) : Submodule ℂ (MvPolynomial (Fin n) ℂ ⧸ I)

noncomputable def polyRepresentation {n : ℕ} {G : Type u_1} [Group G] (algAct : G →* MvPolynomial (Fin n) ℂ ≃ₐ[ℂ] MvPolynomial (Fin n) ℂ) : Representation ℂ G (MvPolynomial (Fin n) ℂ)

structure CSTPartIIData : Type (max (u_1 + 1) (u_2 + 1))

• n : ℕ
• G : Type u_1
• instGroup : Group self.G
• instFintype : Fintype self.G
• instDecEq : DecidableEq self.G
• linearAction : self.G →* (Fin self.n → ℂ) ≃ₗ[ℂ] Fin self.n → ℂ
• is_reflection_group : IsComplexReflectionGroup self.G self.linearAction
• algAct : self.G →* MvPolynomial (Fin self.n) ℂ ≃ₐ[ℂ] MvPolynomial (Fin self.n) ℂ
• invariantSubalgebra : Subalgebra ℂ (MvPolynomial (Fin self.n) ℂ)
• mem_invariant_iff (p : MvPolynomial (Fin self.n) ℂ) : p ∈ self.invariantSubalgebra ↔ ∀ (g : self.G), (self.algAct g) p = p
• basicInvariants : Fin self.n → ↥self.invariantSubalgebra
• alg_independent : AlgebraicIndependent ℂ self.basicInvariants
• generators_generate : Algebra.adjoin ℂ (Set.range self.basicInvariants) = ⊤
• degrees : Fin self.n → ℕ
• basicInvariants_homogeneous (i : Fin self.n) : (↑(self.basicInvariants i)).IsHomogeneous (self.degrees i)
• basicInvariants_vanish (v : Fin self.n → ℂ) : (∀ (i : Fin self.n), (MvPolynomial.eval v) ↑(self.basicInvariants i) = 0) → v = 0
• R₀ : Type u_2
• instR₀AddCommGroup : AddCommGroup self.R₀
• instR₀Module : Module ℂ self.R₀
• instR₀FiniteDimensional : FiniteDimensional ℂ self.R₀
• R₀Action : Representation ℂ self.G self.R₀
• R₀_quotient_iso : self.R₀ ≃ₗ[ℂ] MvPolynomial (Fin self.n) ℂ ⧸ Ideal.span (Set.range fun (i : Fin self.n) => ↑(self.basicInvariants i))
• hilbertR₀ : PowerSeries ℤ
• hilbertR₀_coeff_eq (N : ℕ) : (PowerSeries.coeff N) self.hilbertR₀ = ↑(Module.finrank ℂ ↥(quotientGradedComponent self.n (Ideal.span (Set.range fun (i : Fin self.n) => ↑(self.basicInvariants i))) N))

noncomputable def CSTPartIIData.polyRep (cst : CSTPartIIData) : Representation ℂ cst.G (MvPolynomial (Fin cst.n) ℂ)

theorem cst_pos_degrees (cst : CSTPartIIData) (i : Fin cst.n) : 0 < cst.degrees i

theorem cst_finite_over_invariants (cst : CSTPartIIData) : Module.Finite (↥(Algebra.adjoin ℂ (Set.range fun (i : Fin cst.n) => ↑(cst.basicInvariants i)))) (MvPolynomial (Fin cst.n) ℂ)

theorem qIntegerCST_eq_qAnalog (d : ℕ) : qIntegerCST d = qAnalog d

theorem quotientGradedComponent_eq_quotientHomogeneousSubmodule (n : ℕ) (I : Ideal (MvPolynomial (Fin n) ℂ)) (N : ℕ) : quotientGradedComponent n I N = quotientHomogeneousSubmodule ℂ n I N

theorem isHomogeneous_to_coeff_form {n : ℕ} {p : MvPolynomial (Fin n) ℂ} {d : ℕ} (hp : p.IsHomogeneous d) (m : Fin n →₀ ℕ) : MvPolynomial.coeff m p ≠ 0 → (m.sum fun (x : Fin n) (e : ℕ) => e) = d

theorem cst_hilbert_series_helper (cst : CSTPartIIData) (N : ℕ) : ↑(Module.finrank ℂ ↥(quotientGradedComponent cst.n (Ideal.span (Set.range fun (i : Fin cst.n) => ↑(cst.basicInvariants i))) N)) = (PowerSeries.coeff N) (∏ i : Fin cst.n, qIntegerCST (cst.degrees i))

noncomputable def qIntPoly (d : ℕ) : Polynomial ℤ

theorem qIntPoly_coe_eq_qIntegerCST (d : ℕ) : ↑(qIntPoly d) = qIntegerCST d

theorem qIntPoly_eval_one (d : ℕ) : Polynomial.eval 1 (qIntPoly d) = ↑d

theorem prod_qIntPoly_coe_eq_prod_qIntegerCST {n : ℕ} (degrees : Fin n → ℕ) : ↑(∏ i : Fin n, qIntPoly (degrees i)) = ∏ i : Fin n, qIntegerCST (degrees i)

theorem prod_qIntCST_coeff_eq_poly_coeff {n : ℕ} (degrees : Fin n → ℕ) (N : ℕ) : (PowerSeries.coeff N) (∏ i : Fin n, qIntegerCST (degrees i)) = (∏ i : Fin n, qIntPoly (degrees i)).coeff N

theorem sum_poly_coeff_eq_eval_one {p : Polynomial ℤ} {B : ℕ} (hB : p.natDegree < B) : ∑ i ∈ Finset.range B, p.coeff i = Polynomial.eval 1 p

theorem sum_prod_qIntCST_coeff_eq_prod_degrees {n : ℕ} (degrees : Fin n → ℕ) {B : ℕ} (hB : (∏ i : Fin n, qIntPoly (degrees i)).natDegree < B) : ∑ N ∈ Finset.range B, (PowerSeries.coeff N) (∏ i : Fin n, qIntegerCST (degrees i)) = ↑(∏ i : Fin n, degrees i)

theorem quotient_finrank_eq_sum_graded (n : ℕ) (I : Ideal (MvPolynomial (Fin n) ℂ)) [FiniteDimensional ℂ (MvPolynomial (Fin n) ℂ ⧸ I)] (D : ℕ) : ∃ (B : ℕ), D < B ∧ Module.finrank ℂ (MvPolynomial (Fin n) ℂ ⧸ I) = ∑ N ∈ Finset.range B, Module.finrank ℂ ↥(quotientGradedComponent n I N)

theorem graded_decomp_finrank (cst : CSTPartIIData) : ∃ (B : ℕ), (∏ i : Fin cst.n, qIntPoly (cst.degrees i)).natDegree < B ∧ Module.finrank ℂ cst.R₀ = ∑ N ∈ Finset.range B, Module.finrank ℂ ↥(quotientGradedComponent cst.n (Ideal.span (Set.range fun (i : Fin cst.n) => ↑(cst.basicInvariants i))) N)

theorem cst_dim_R0_eq_prod_helper (cst : CSTPartIIData) : Module.finrank ℂ cst.R₀ = ∏ i : Fin cst.n, cst.degrees i

theorem galois_theory_R0_iso (cst : CSTPartIIData) : Nonempty (cst.R₀Action.Equiv (Representation.leftRegular ℂ cst.G))

theorem cst_R0_regular_rep_helper (cst : CSTPartIIData) : Nonempty (cst.R₀Action.Equiv (Representation.leftRegular ℂ cst.G))

theorem cst_hom_graded_projective_data (cst : CSTPartIIData) (W : Type u_1) [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W] (ρ : Representation ℂ cst.G W) [ρ.IsIrreducible] [Module ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants] : ∃ (𝒮 : ℕ → Submodule ℂ ↥cst.invariantSubalgebra) (hGA : GradedAlgebra 𝒮) (_ : IsConnectedGrading ℂ (↥cst.invariantSubalgebra) 𝒮) (ℳ : ℕ → Submodule ℂ ↥(ρ.linHom cst.polyRep).invariants) (x : IsScalarTower ℂ ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants) (_ : Module.Projective ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants), IsGradedSModule 𝒮 ℳ

theorem cst_hom_is_free_helper (cst : CSTPartIIData) (W : Type u_1) [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W] (ρ : Representation ℂ cst.G W) [ρ.IsIrreducible] [Module ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants] : Module.Free ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants

theorem galois_theory_hom_rank (cst : CSTPartIIData) (W : Type u_1) [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W] (ρ : Representation ℂ cst.G W) [ρ.IsIrreducible] [Module ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants] (hfree : Module.Free ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants) : Module.finrank ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants = Module.finrank ℂ W

theorem cst_hom_rank_eq_dim_helper (cst : CSTPartIIData) (W : Type u_1) [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W] (ρ : Representation ℂ cst.G W) [ρ.IsIrreducible] [Module ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants] (hfree : Module.Free ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants) : Module.finrank ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants = Module.finrank ℂ W

theorem cst_hom_free_rank_helper (cst : CSTPartIIData) (W : Type u_1) [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W] (ρ : Representation ℂ cst.G W) [ρ.IsIrreducible] [Module ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants] : Module.Free ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants ∧ (Module.Free ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants → Module.finrank ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants = Module.finrank ℂ W)

theorem cst_theorem_12_2_proof (cst : CSTPartIIData) : (∀ (N : ℕ), ↑(Module.finrank ℂ ↥(quotientGradedComponent cst.n (Ideal.span (Set.range fun (i : Fin cst.n) => ↑(cst.basicInvariants i))) N)) = (PowerSeries.coeff N) (∏ i : Fin cst.n, qIntegerCST (cst.degrees i))) ∧ Module.finrank ℂ cst.R₀ = ∏ i : Fin cst.n, cst.degrees i ∧ Nonempty (cst.R₀Action.Equiv (Representation.leftRegular ℂ cst.G)) ∧ ∀ (W : Type u_1) [inst : AddCommGroup W] [inst_1 : Module ℂ W] [FiniteDimensional ℂ W] (ρ : Representation ℂ cst.G W) [ρ.IsIrreducible] [inst_4 : Module ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants], Module.Free ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants ∧ (Module.Free ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants → Module.finrank ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants = Module.finrank ℂ W)

theorem cst_regular_sequence_graded_dim (cst : CSTPartIIData) (N : ℕ) : ↑(Module.finrank ℂ ↥(quotientGradedComponent cst.n (Ideal.span (Set.range fun (i : Fin cst.n) => ↑(cst.basicInvariants i))) N)) = (PowerSeries.coeff N) (∏ i : Fin cst.n, qIntegerCST (cst.degrees i))

theorem cst_finrank_R0_eq_prod_degrees (cst : CSTPartIIData) : Module.finrank ℂ cst.R₀ = ∏ i : Fin cst.n, cst.degrees i

theorem cst_R0_is_regular_rep (cst : CSTPartIIData) : Nonempty (cst.R₀Action.Equiv (Representation.leftRegular ℂ cst.G))

theorem cst_finrank_R0_eq_card (cst : CSTPartIIData) : Module.finrank ℂ cst.R₀ = Fintype.card cst.G

theorem cst_partII_hom_free_and_rank (cst : CSTPartIIData) (W : Type u_1) [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W] (ρ : Representation ℂ cst.G W) [ρ.IsIrreducible] [Module ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants] : Module.Free ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants ∧ (Module.Free ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants → Module.finrank ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants = Module.finrank ℂ W)

theorem cst_partII_R0_regular_rep (cst : CSTPartIIData) : Nonempty (cst.R₀Action.Equiv (Representation.leftRegular ℂ cst.G))

theorem cst_partII_prod_degrees_eq_card (cst : CSTPartIIData) : ∏ i : Fin cst.n, cst.degrees i = Fintype.card cst.G

theorem cst_partII_hilbert_polynomial (cst : CSTPartIIData) : cst.hilbertR₀ = ∏ i : Fin cst.n, qIntegerCST (cst.degrees i)

theorem cst_partII (cst : CSTPartIIData) : (∀ (W : Type u_1) [inst : AddCommGroup W] [inst_1 : Module ℂ W] [FiniteDimensional ℂ W] (ρ : Representation ℂ cst.G W) [ρ.IsIrreducible] [inst_4 : Module ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants], Module.Free ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants ∧ (Module.Free ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants → Module.finrank ↥cst.invariantSubalgebra ↥(ρ.linHom cst.polyRep).invariants = Module.finrank ℂ W)) ∧ Nonempty (cst.R₀Action.Equiv (Representation.leftRegular ℂ cst.G)) ∧ ∏ i : Fin cst.n, cst.degrees i = Fintype.card cst.G ∧ cst.hilbertR₀ = ∏ i : Fin cst.n, qIntegerCST (cst.degrees i)