def IsRegularSequence {A : Type u_1} [CommRing A] {m : ℕ} (f : Fin m → A) : Prop

structure IsGradedSModule {k : Type u_1} {S : Type u_2} {M : Type u_3} [CommRing k] [Ring S] [Algebra k S] [AddCommGroup M] [Module S M] [Module k M] [IsScalarTower k S M] (𝒮 : ℕ → Submodule k S) [GradedAlgebra 𝒮] (ℳ : ℕ → Submodule k M) : Prop

• internal : DirectSum.IsInternal ℳ
• smul_mem (i j : ℕ) (s : S) (m : M) : s ∈ 𝒮 j → m ∈ ℳ i → s • m ∈ ℳ (i + j)

def IsConnectedGrading (k : Type u_1) (S : Type u_2) [CommRing k] [Ring S] [Algebra k S] (𝒮 : ℕ → Submodule k S) [GradedAlgebra 𝒮] : Prop

def augmentationIdealGraded {k : Type u_1} {S : Type u_2} [CommRing k] [CommRing S] [Algebra k S] (𝒮 : ℕ → Submodule k S) [GradedAlgebra 𝒮] : Ideal S

theorem isHomogeneous_augmentationIdealGraded {k : Type u_1} {S : Type u_2} [CommRing k] [CommRing S] [Algebra k S] (𝒮 : ℕ → Submodule k S) [GradedAlgebra 𝒮] : Ideal.IsHomogeneous 𝒮 (augmentationIdealGraded 𝒮)

theorem augmentationIdealGraded_component_mem {k : Type u_1} {S : Type u_2} [CommRing k] [CommRing S] [Algebra k S] (𝒮 : ℕ → Submodule k S) [GradedAlgebra 𝒮] (r : S) (hr : r ∈ augmentationIdealGraded 𝒮) (j : ℕ) : ↑(((DirectSum.decompose 𝒮) r) j) ∈ augmentationIdealGraded 𝒮

noncomputable def hilbertSeries {k : Type u_1} {M : Type u_2} [Field k] [AddCommGroup M] [Module k M] (ℳ : ℕ → Submodule k M) : PowerSeries ℤ

noncomputable def augmentation_ideal_poly (k : Type u_1) [Field k] (n : ℕ) : Ideal (MvPolynomial (Fin n) k)

theorem homog_in_aug_smul {k' : Type u_2} {S : Type u_3} [Field k'] [CommRing S] [Algebra k' S] (𝒮 : ℕ → Submodule k' S) [GradedAlgebra 𝒮] {M : Type u_4} [AddCommGroup M] [Module S M] [Module k' M] [IsScalarTower k' S M] (ℳ : ℕ → Submodule k' M) (hgr : IsGradedSModule 𝒮 ℳ) (d : ℕ) (x : M) (hxd : x ∈ ℳ d) (hxP : x ∈ augmentationIdealGraded 𝒮 • ⊤) : x ∈ Submodule.span k' (⋃ (j : ℕ), ⋃ (_ : 0 < j), ⋃ (i : ℕ), ⋃ (_ : i + j = d), Set.image2 HSMul.hSMul ↑(𝒮 j) ↑(ℳ i))

theorem exists_homogeneous_span_quotient {k' : Type u_2} {S : Type u_3} [Field k'] [CommRing S] [Algebra k' S] (𝒮 : ℕ → Submodule k' S) [GradedAlgebra 𝒮] {M : Type u_4} [AddCommGroup M] [Module S M] [Module k' M] [IsScalarTower k' S M] (ℳ : ℕ → Submodule k' M) (hgr : IsGradedSModule 𝒮 ℳ) (hfin : FiniteDimensional k' (M ⧸ augmentationIdealGraded 𝒮 • ⊤)) : ∃ (T : Finset M), (∀ t ∈ T, ∃ (d : ℕ), t ∈ ℳ d) ∧ Submodule.span k' (⇑(augmentationIdealGraded 𝒮 • ⊤).mkQ '' ↑T) = ⊤

theorem homog_smul_component_mem_aug {k' : Type u_2} {S : Type u_3} [Field k'] [CommRing S] [Algebra k' S] (𝒮 : ℕ → Submodule k' S) [GradedAlgebra 𝒮] {M : Type u_4} [AddCommGroup M] [Module S M] [Module k' M] [IsScalarTower k' S M] (ℳ : ℕ → Submodule k' M) (hgr : IsGradedSModule 𝒮 ℳ) [DirectSum.Decomposition ℳ] (d j : ℕ) (rj : S) (hrj_homog : rj ∈ 𝒮 j) (hrj_aug : rj ∈ augmentationIdealGraded 𝒮) (n : M) : ↑(((DirectSum.decompose ℳ) (rj • n)) d) ∈ augmentationIdealGraded 𝒮 • ⊤

theorem aug_smul_graded_component {k' : Type u_2} {S : Type u_3} [Field k'] [CommRing S] [Algebra k' S] (𝒮 : ℕ → Submodule k' S) [GradedAlgebra 𝒮] {M : Type u_4} [AddCommGroup M] [Module S M] [Module k' M] [IsScalarTower k' S M] (ℳ : ℕ → Submodule k' M) (hgr : IsGradedSModule 𝒮 ℳ) [DirectSum.Decomposition ℳ] (d : ℕ) (z : M) (hz : z ∈ augmentationIdealGraded 𝒮 • ⊤) : ↑(((DirectSum.decompose ℳ) z) d) ∈ augmentationIdealGraded 𝒮 • ⊤

theorem decompose_mod_P {k' : Type u_2} {S : Type u_3} [Field k'] [CommRing S] [Algebra k' S] (𝒮 : ℕ → Submodule k' S) [GradedAlgebra 𝒮] {M : Type u_4} [AddCommGroup M] [Module S M] [Module k' M] [IsScalarTower k' S M] (ℳ : ℕ → Submodule k' M) (hgr : IsGradedSModule 𝒮 ℳ) (T : Finset M) (hThom : ∀ t ∈ T, ∃ (d : ℕ), t ∈ ℳ d) (hTspan : Submodule.span k' (⇑(augmentationIdealGraded 𝒮 • ⊤).mkQ '' ↑T) = ⊤) (d : ℕ) (m : M) (hm : m ∈ ℳ d) : ∃ v ∈ Submodule.span k' (↑T ∩ ↑(ℳ d)), m - v ∈ ℳ d ∧ m - v ∈ augmentationIdealGraded 𝒮 • ⊤

theorem lemma_12_3_i_generators {k' : Type u_2} {S : Type u_3} [Field k'] [CommRing S] [Algebra k' S] (𝒮 : ℕ → Submodule k' S) [GradedAlgebra 𝒮] (hconn : IsConnectedGrading k' S 𝒮) {M : Type u_4} [AddCommGroup M] [Module S M] [Module k' M] [IsScalarTower k' S M] (ℳ : ℕ → Submodule k' M) (hgr : IsGradedSModule 𝒮 ℳ) (hfin : FiniteDimensional k' (M ⧸ augmentationIdealGraded 𝒮 • ⊤)) : Module.Finite S M

theorem graded_nakayama {k' : Type u_2} {S : Type u_3} [Field k'] [CommRing S] [Algebra k' S] (𝒮 : ℕ → Submodule k' S) [GradedAlgebra 𝒮] (_hconn : IsConnectedGrading k' S 𝒮) {N : Type u_4} [AddCommGroup N] [Module S N] [Module k' N] [IsScalarTower k' S N] (𝒩 : ℕ → Submodule k' N) (hgr : IsGradedSModule 𝒮 𝒩) (hdeg0 : 𝒩 0 = ⊥) (hSN : ∀ (d : ℕ), ∀ n ∈ 𝒩 d, n ∈ Submodule.span k' (⋃ (j : ℕ), ⋃ (_ : 0 < j), ⋃ (i : ℕ), ⋃ (_ : i + j = d), Set.image2 HSMul.hSMul ↑(𝒮 j) ↑(𝒩 i))) (n : N) : n = 0

theorem kernel_has_graded_nakayama_data {k' : Type u_2} {S : Type u_3} [Field k'] [CommRing S] [Algebra k' S] (𝒮 : ℕ → Submodule k' S) [GradedAlgebra 𝒮] (hconn : IsConnectedGrading k' S 𝒮) {M : Type u_4} [AddCommGroup M] [Module S M] [Module k' M] [IsScalarTower k' S M] (ℳ : ℕ → Submodule k' M) (hgr : IsGradedSModule 𝒮 ℳ) {F : Type u_5} [AddCommGroup F] [Module S F] [Module k' F] [IsScalarTower k' S F] [Module.Free S F] (iMF : M →ₗ[S] F) (sFM : F →ₗ[S] M) (h_split : sFM ∘ₗ iMF = LinearMap.id) : ∃ (𝒦 : ℕ → Submodule k' ↥sFM.ker), IsGradedSModule 𝒮 𝒦 ∧ 𝒦 0 = ⊥ ∧ ∀ (d : ℕ), ∀ n ∈ 𝒦 d, n ∈ Submodule.span k' (⋃ (j : ℕ), ⋃ (_ : 0 < j), ⋃ (i : ℕ), ⋃ (_ : i + j = d), Set.image2 HSMul.hSMul ↑(𝒮 j) ↑(𝒦 i))

theorem kernel_vanishes_of_graded_split {k' : Type u_2} {S : Type u_3} [Field k'] [CommRing S] [Algebra k' S] (𝒮 : ℕ → Submodule k' S) [GradedAlgebra 𝒮] (hconn : IsConnectedGrading k' S 𝒮) {M : Type u_4} [AddCommGroup M] [Module S M] [Module k' M] [IsScalarTower k' S M] (ℳ : ℕ → Submodule k' M) (hgr : IsGradedSModule 𝒮 ℳ) {F : Type u_5} [AddCommMonoid F] [Module S F] [Module.Free S F] (iMF : M →ₗ[S] F) (sFM : F →ₗ[S] M) (h_split : sFM ∘ₗ iMF = LinearMap.id) : Function.Injective ⇑sFM

theorem graded_projective_is_free {k' : Type u_2} {S : Type u_3} [Field k'] [CommRing S] [Algebra k' S] (𝒮 : ℕ → Submodule k' S) [GradedAlgebra 𝒮] (hconn : IsConnectedGrading k' S 𝒮) {M : Type u_4} [AddCommGroup M] [Module S M] [Module k' M] [IsScalarTower k' S M] [Module.Projective S M] (ℳ : ℕ → Submodule k' M) (hgr : IsGradedSModule 𝒮 ℳ) : Module.Free S M

def quotientGrading {k' : Type u_2} {S : Type u_3} [CommRing k'] [CommRing S] [Algebra k' S] {M : Type u_4} [AddCommGroup M] [Module S M] [Module k' M] [IsScalarTower k' S M] (𝒮 : ℕ → Submodule k' S) [GradedAlgebra 𝒮] (ℳ : ℕ → Submodule k' M) (i : ℕ) : Submodule k' (M ⧸ augmentationIdealGraded 𝒮 • ⊤)

theorem graded_free_module_dim_conv {k' : Type u_2} {S : Type u_3} [Field k'] [CommRing S] [Algebra k' S] (𝒮 : ℕ → Submodule k' S) [GradedAlgebra 𝒮] (hconn : IsConnectedGrading k' S 𝒮) {M : Type u_4} [AddCommGroup M] [Module S M] [Module k' M] [IsScalarTower k' S M] [Module.Projective S M] (ℳ : ℕ → Submodule k' M) (hgr : IsGradedSModule 𝒮 ℳ) (hfindim : ∀ (i : ℕ), FiniteDimensional k' ↥(ℳ i)) (n : ℕ) : ↑(Module.finrank k' ↥(ℳ n)) = ∑ p ∈ Finset.antidiagonal n, ↑(Module.finrank k' ↥(𝒮 p.1)) * ↑(Module.finrank k' ↥(quotientGrading 𝒮 ℳ p.2))

theorem lemma_12_3_ii_hilbert_series {k' : Type u_2} {S : Type u_3} [Field k'] [CommRing S] [Algebra k' S] (𝒮 : ℕ → Submodule k' S) [GradedAlgebra 𝒮] (hconn : IsConnectedGrading k' S 𝒮) {M : Type u_4} [AddCommGroup M] [Module S M] [Module k' M] [IsScalarTower k' S M] [Module.Projective S M] (ℳ : ℕ → Submodule k' M) (hgr : IsGradedSModule 𝒮 ℳ) (hfindim : ∀ (i : ℕ), FiniteDimensional k' ↥(ℳ i)) : hilbertSeries ℳ = hilbertSeries 𝒮 * hilbertSeries (quotientGrading 𝒮 ℳ)

theorem lemma_12_3_ii_graded_projective_free {k' : Type u_2} {S : Type u_3} [Field k'] [CommRing S] [Algebra k' S] (𝒮 : ℕ → Submodule k' S) [GradedAlgebra 𝒮] (hconn : IsConnectedGrading k' S 𝒮) {M : Type u_4} [AddCommGroup M] [Module S M] [Module k' M] [IsScalarTower k' S M] [Module.Projective S M] (ℳ : ℕ → Submodule k' M) (hgr : IsGradedSModule 𝒮 ℳ) (hfindim : ∀ (i : ℕ), FiniteDimensional k' ↥(ℳ i)) : Module.Free S M ∧ hilbertSeries ℳ = hilbertSeries (quotientGrading 𝒮 ℳ) * hilbertSeries 𝒮

theorem mvpoly_connected_grading (k : Type u_1) [Field k] (n : ℕ) : IsConnectedGrading k (MvPolynomial (Fin n) k) (MvPolynomial.homogeneousSubmodule (Fin n) k)

structure KoszulComplex (k : Type u_2) [Field k] (n : ℕ) : Type u_2

• rank (p : ℕ) (hp : p ≤ n) : ℕ
• rank_eq (p : ℕ) (hp : p ≤ n) : self.rank p hp = n.choose p
• differential (p : ℕ) (hp : 0 < p) (hp' : p ≤ n) : (Fin (self.rank p hp') → MvPolynomial (Fin n) k) →ₗ[MvPolynomial (Fin n) k] Fin (self.rank (p - 1) ⋯) → MvPolynomial (Fin n) k
• d_squared_zero (p : ℕ) (hp : 1 < p) (hp' : p ≤ n) : self.differential (p - 1) ⋯ ⋯ ∘ₗ self.differential p ⋯ hp' = 0

theorem split_exact_tensor_preserves_resolution (k : Type u_2) [Field k] (n : ℕ) (M : Type u_3) [AddCommGroup M] [Module (MvPolynomial (Fin n) k) M] : ∃ (B_M : Type u_4) (d : (i : ℕ) → i < n → (Fin (n.choose (i + 1)) × B_M →₀ MvPolynomial (Fin n) k) →ₗ[MvPolynomial (Fin n) k] Fin (n.choose i) × B_M →₀ MvPolynomial (Fin n) k) (ε : (Fin (n.choose 0) × B_M →₀ MvPolynomial (Fin n) k) →ₗ[MvPolynomial (Fin n) k] M), Function.Surjective ⇑ε ∧ (∀ (hn : 0 < n), ε.ker = (d 0 hn).range) ∧ (n = 0 → ε.ker = ⊥) ∧ (∀ (i : ℕ) (hi : i < n) (hi' : i + 1 < n), (d i hi).ker = (d (i + 1) hi').range) ∧ ∀ (hn : 0 < n), Function.Injective ⇑(d (n - 1) ⋯)

theorem prop_12_4_ext_vanishing (k : Type u_1) [Field k] (n : ℕ) (M : Type u_2) [AddCommGroup M] [Module (MvPolynomial (Fin n) k) M] : ∃ (ι : Fin (n + 1) → Type u_3) (d : (i : ℕ) → (x : i < n) → (ι ⟨i + 1, ⋯⟩ →₀ MvPolynomial (Fin n) k) →ₗ[MvPolynomial (Fin n) k] ι ⟨i, ⋯⟩ →₀ MvPolynomial (Fin n) k) (ε : (ι ⟨0, ⋯⟩ →₀ MvPolynomial (Fin n) k) →ₗ[MvPolynomial (Fin n) k] M), Function.Surjective ⇑ε ∧ (∀ (hn : 0 < n), ε.ker = (d 0 hn).range) ∧ (n = 0 → ε.ker = ⊥) ∧ (∀ (i : ℕ) (hi : i < n) (hi' : i + 1 < n), (d i hi).ker = (d (i + 1) hi').range) ∧ ∀ (hn : 0 < n), Function.Injective ⇑(d (n - 1) ⋯)

theorem syzygy_ext_vanishing (k : Type u_2) [Field k] (n : ℕ) (M : Type u_3) [AddCommGroup M] [Module (MvPolynomial (Fin n) k) M] [Module.Finite (MvPolynomial (Fin n) k) M] : ∃ (r : Fin (n + 1) → ℕ) (d : (i : ℕ) → (x : i < n) → (Fin (r ⟨i + 1, ⋯⟩) → MvPolynomial (Fin n) k) →ₗ[MvPolynomial (Fin n) k] Fin (r ⟨i, ⋯⟩) → MvPolynomial (Fin n) k) (ε : (Fin (r ⟨0, ⋯⟩) → MvPolynomial (Fin n) k) →ₗ[MvPolynomial (Fin n) k] M), Function.Surjective ⇑ε ∧ (∀ (hn : 0 < n), ε.ker = (d 0 hn).range) ∧ (∀ (i : ℕ) (hi : i < n) (hi' : i + 1 < n), (d i hi).ker = (d (i + 1) hi').range) ∧ ∀ (hn : 0 < n), Function.Injective ⇑(d (n - 1) ⋯)

theorem nth_syzygy_is_free (k : Type u_1) [Field k] (n : ℕ) (M : Type u_2) [AddCommGroup M] [Module (MvPolynomial (Fin n) k) M] [Module.Finite (MvPolynomial (Fin n) k) M] : ∃ (r : Fin (n + 1) → ℕ) (d : (i : ℕ) → (x : i < n) → (Fin (r ⟨i + 1, ⋯⟩) → MvPolynomial (Fin n) k) →ₗ[MvPolynomial (Fin n) k] Fin (r ⟨i, ⋯⟩) → MvPolynomial (Fin n) k) (ε : (Fin (r ⟨0, ⋯⟩) → MvPolynomial (Fin n) k) →ₗ[MvPolynomial (Fin n) k] M), Function.Surjective ⇑ε ∧ (∀ (hn : 0 < n), ε.ker = (d 0 hn).range) ∧ (∀ (i : ℕ) (hi : i < n) (hi' : i + 1 < n), (d i hi).ker = (d (i + 1) hi').range) ∧ ∀ (hn : 0 < n), Function.Injective ⇑(d (n - 1) ⋯)

def freeModuleGrading (k : Type u_1) [Field k] (n : ℕ) {m : ℕ} (d : ℕ) : Submodule k (Fin m → MvPolynomial (Fin n) k)

def twistedFreeModuleGrading (k : Type u_1) [Field k] (n : ℕ) {m : ℕ} (degrees : Fin m → ℕ) (p : ℕ) : Submodule k (Fin m → MvPolynomial (Fin n) k)

theorem mem_finsuppAntidiag_iff_degree (n d : ℕ) (f : Fin n →₀ ℕ) : f ∈ Finset.univ.finsuppAntidiag d ↔ Finsupp.degree f = d

@[implicit_reducible]

noncomputable instance fintypeFinsuppDegreeEq (n d : ℕ) : Fintype ↑{s : Fin n →₀ ℕ | Finsupp.degree s = d}

instance instModuleFiniteHomogSub (k : Type u_1) [Field k] (n d : ℕ) : Module.Finite k ↥(MvPolynomial.homogeneousSubmodule (Fin n) k d)

noncomputable def freeModuleGradingEquiv (k : Type u_1) [Field k] (n m d : ℕ) : ↥(freeModuleGrading k n d) ≃ₗ[k] Fin m → ↥(MvPolynomial.homogeneousSubmodule (Fin n) k d)

theorem finrank_homogeneousSubmodule_eq (k : Type u_1) [Field k] (n d : ℕ) : Module.finrank k ↥(MvPolynomial.homogeneousSubmodule (Fin n) k d) = n.multichoose d

theorem hilbertSeries_homogeneousSubmodule (k : Type u_1) [Field k] (n : ℕ) : hilbertSeries (MvPolynomial.homogeneousSubmodule (Fin n) k) = PowerSeries.mk 1 ^ n

theorem hilbert_series_twisted_free_module_poly (k : Type u_1) [Field k] (n : ℕ) {m : ℕ} (degrees : Fin m → ℕ) : ∃ (p : Polynomial ℤ), (1 - PowerSeries.X) ^ n * hilbertSeries (twistedFreeModuleGrading k n degrees) = ↑p

theorem hilbert_syzygy_graded_free_resolution (k : Type u_1) [Field k] (n : ℕ) {M : Type u_2} [AddCommGroup M] [Module (MvPolynomial (Fin n) k) M] [Module k M] [IsScalarTower k (MvPolynomial (Fin n) k) M] [Module.Finite (MvPolynomial (Fin n) k) M] (ℳ : ℕ → Submodule k M) (hgr : IsGradedSModule (MvPolynomial.homogeneousSubmodule (Fin n) k) ℳ) : ∃ (r : Fin (n + 1) → ℕ) (shifts : (i : Fin (n + 1)) → Fin (r i) → ℕ) (d : (i : ℕ) → (hi : i < n) → (Fin (r ⟨i + 1, ⋯⟩) → MvPolynomial (Fin n) k) →ₗ[MvPolynomial (Fin n) k] Fin (r ⟨i, ⋯⟩) → MvPolynomial (Fin n) k) (ε : (Fin (r ⟨0, ⋯⟩) → MvPolynomial (Fin n) k) →ₗ[MvPolynomial (Fin n) k] M), Function.Surjective ⇑ε ∧ (∀ (hn : 0 < n), ε.ker = (d 0 hn).range) ∧ (n = 0 → ε.ker = ⊥) ∧ (∀ (i : ℕ) (hi : i < n) (hi' : i + 1 < n), (d i hi).ker = (d (i + 1) hi').range) ∧ (∀ (hn : 0 < n), Function.Injective ⇑(d (n - 1) ⋯)) ∧ (∀ (i : ℕ) (hi : i < n) (p : ℕ), ∀ v ∈ ↑(twistedFreeModuleGrading k n (shifts ⟨i + 1, ⋯⟩) p), (d i hi) v ∈ ↑(twistedFreeModuleGrading k n (shifts ⟨i, ⋯⟩) p)) ∧ ∀ (p : ℕ), ∀ v ∈ ↑(twistedFreeModuleGrading k n (shifts ⟨0, ⋯⟩) p), ε v ∈ ℳ p

theorem graded_euler_characteristic_telescope (k : Type u_1) [Field k] (n : ℕ) {M : Type u_2} [AddCommGroup M] [Module (MvPolynomial (Fin n) k) M] [Module k M] [IsScalarTower k (MvPolynomial (Fin n) k) M] (ℳ : ℕ → Submodule k M) (hgr : IsGradedSModule (MvPolynomial.homogeneousSubmodule (Fin n) k) ℳ) (hfindim : ∀ (i : ℕ), FiniteDimensional k ↥(ℳ i)) (r : Fin (n + 1) → ℕ) (shifts : (i : Fin (n + 1)) → Fin (r i) → ℕ) (d : (i : ℕ) → (hi : i < n) → (Fin (r ⟨i + 1, ⋯⟩) → MvPolynomial (Fin n) k) →ₗ[MvPolynomial (Fin n) k] Fin (r ⟨i, ⋯⟩) → MvPolynomial (Fin n) k) (ε : (Fin (r ⟨0, ⋯⟩) → MvPolynomial (Fin n) k) →ₗ[MvPolynomial (Fin n) k] M) (hε_surj : Function.Surjective ⇑ε) (hε_exact : ∀ (hn : 0 < n), ε.ker = (d 0 hn).range) (hε_zero : n = 0 → ε.ker = ⊥) (hd_exact : ∀ (i : ℕ) (hi : i < n) (hi' : i + 1 < n), (d i hi).ker = (d (i + 1) hi').range) (hd_inj : ∀ (hn : 0 < n), Function.Injective ⇑(d (n - 1) ⋯)) (hd_graded : ∀ (i : ℕ) (hi : i < n) (p : ℕ), ∀ v ∈ ↑(twistedFreeModuleGrading k n (shifts ⟨i + 1, ⋯⟩) p), (d i hi) v ∈ ↑(twistedFreeModuleGrading k n (shifts ⟨i, ⋯⟩) p)) (hε_graded : ∀ (p : ℕ), ∀ v ∈ ↑(twistedFreeModuleGrading k n (shifts ⟨0, ⋯⟩) p), ε v ∈ ℳ p) (p : ℕ) : ∃ (b : ℕ → ℤ), b 0 = ↑(Module.finrank k ↥(ℳ p)) ∧ b (n + 1) = 0 ∧ ∀ (j : Fin (n + 1)), ↑(Module.finrank k ↥(twistedFreeModuleGrading k n (shifts j) p)) = b ↑j + b (↑j + 1)

theorem alternating_sum_general' (nn : ℕ) (b : ℕ → ℤ) : ∑ j : Fin (nn + 1), (-1) ^ ↑j * (b ↑j + b (↑j + 1)) = b 0 + (-1) ^ nn * b (nn + 1)

theorem alternating_sum_eq' (nn : ℕ) (a : Fin (nn + 1) → ℤ) (target : ℤ) (b : ℕ → ℤ) (hb0 : b 0 = target) (hbn : b (nn + 1) = 0) (hab : ∀ (j : Fin (nn + 1)), a j = b ↑j + b (↑j + 1)) : ∑ j : Fin (nn + 1), (-1) ^ ↑j * a j = target

theorem resolution_hilbert_alternating_sum (k : Type u_1) [Field k] (n : ℕ) {M : Type u_2} [AddCommGroup M] [Module (MvPolynomial (Fin n) k) M] [Module k M] [IsScalarTower k (MvPolynomial (Fin n) k) M] (ℳ : ℕ → Submodule k M) (hgr : IsGradedSModule (MvPolynomial.homogeneousSubmodule (Fin n) k) ℳ) (hfindim : ∀ (i : ℕ), FiniteDimensional k ↥(ℳ i)) (r : Fin (n + 1) → ℕ) (shifts : (i : Fin (n + 1)) → Fin (r i) → ℕ) (d : (i : ℕ) → (hi : i < n) → (Fin (r ⟨i + 1, ⋯⟩) → MvPolynomial (Fin n) k) →ₗ[MvPolynomial (Fin n) k] Fin (r ⟨i, ⋯⟩) → MvPolynomial (Fin n) k) (ε : (Fin (r ⟨0, ⋯⟩) → MvPolynomial (Fin n) k) →ₗ[MvPolynomial (Fin n) k] M) (hε_surj : Function.Surjective ⇑ε) (hε_exact : ∀ (hn : 0 < n), ε.ker = (d 0 hn).range) (hε_zero : n = 0 → ε.ker = ⊥) (hd_exact : ∀ (i : ℕ) (hi : i < n) (hi' : i + 1 < n), (d i hi).ker = (d (i + 1) hi').range) (hd_inj : ∀ (hn : 0 < n), Function.Injective ⇑(d (n - 1) ⋯)) (hd_graded : ∀ (i : ℕ) (hi : i < n) (p : ℕ), ∀ v ∈ ↑(twistedFreeModuleGrading k n (shifts ⟨i + 1, ⋯⟩) p), (d i hi) v ∈ ↑(twistedFreeModuleGrading k n (shifts ⟨i, ⋯⟩) p)) (hε_graded : ∀ (p : ℕ), ∀ v ∈ ↑(twistedFreeModuleGrading k n (shifts ⟨0, ⋯⟩) p), ε v ∈ ℳ p) : hilbertSeries ℳ = ∑ j : Fin (n + 1), (-1) ^ ↑j • hilbertSeries (twistedFreeModuleGrading k n (shifts j))

theorem free_resolution_euler_char (k : Type u_1) [Field k] (n : ℕ) {M : Type u_2} [AddCommGroup M] [Module (MvPolynomial (Fin n) k) M] [Module k M] [IsScalarTower k (MvPolynomial (Fin n) k) M] [Module.Finite (MvPolynomial (Fin n) k) M] (ℳ : ℕ → Submodule k M) (hgr : IsGradedSModule (MvPolynomial.homogeneousSubmodule (Fin n) k) ℳ) (hfindim : ∀ (i : ℕ), FiniteDimensional k ↥(ℳ i)) (r : Fin (n + 1) → ℕ) (shifts : (i : Fin (n + 1)) → Fin (r i) → ℕ) (d : (i : ℕ) → (hi : i < n) → (Fin (r ⟨i + 1, ⋯⟩) → MvPolynomial (Fin n) k) →ₗ[MvPolynomial (Fin n) k] Fin (r ⟨i, ⋯⟩) → MvPolynomial (Fin n) k) (ε : (Fin (r ⟨0, ⋯⟩) → MvPolynomial (Fin n) k) →ₗ[MvPolynomial (Fin n) k] M) (hε_surj : Function.Surjective ⇑ε) (hε_exact : ∀ (hn : 0 < n), ε.ker = (d 0 hn).range) (hε_zero : n = 0 → ε.ker = ⊥) (hd_exact : ∀ (i : ℕ) (hi : i < n) (hi' : i + 1 < n), (d i hi).ker = (d (i + 1) hi').range) (hd_inj : ∀ (hn : 0 < n), Function.Injective ⇑(d (n - 1) ⋯)) (hd_graded : ∀ (i : ℕ) (hi : i < n) (p : ℕ), ∀ v ∈ ↑(twistedFreeModuleGrading k n (shifts ⟨i + 1, ⋯⟩) p), (d i hi) v ∈ ↑(twistedFreeModuleGrading k n (shifts ⟨i, ⋯⟩) p)) (hε_graded : ∀ (p : ℕ), ∀ v ∈ ↑(twistedFreeModuleGrading k n (shifts ⟨0, ⋯⟩) p), ε v ∈ ℳ p) : ∃ (p : Polynomial ℤ), (1 - PowerSeries.X) ^ n * hilbertSeries ℳ = ↑p

theorem hilbert_syzygy_theorem (k : Type u_1) [Field k] (n : ℕ) {M : Type u_2} [AddCommGroup M] [Module (MvPolynomial (Fin n) k) M] [Module k M] [IsScalarTower k (MvPolynomial (Fin n) k) M] [Module.Finite (MvPolynomial (Fin n) k) M] (ℳ : ℕ → Submodule k M) (hgr : IsGradedSModule (MvPolynomial.homogeneousSubmodule (Fin n) k) ℳ) (hfindim : ∀ (i : ℕ), FiniteDimensional k ↥(ℳ i)) : ∃ (p : Polynomial ℤ), (1 - PowerSeries.X) ^ n * hilbertSeries ℳ = ↑p

theorem lemma_12_6_krull_dim_quotient {A : Type u_2} [CommRing A] [IsNoetherianRing A] [IsLocalRing A] (f : A) (hf : f ∈ IsLocalRing.maximalIdeal A) : ringKrullDim A ≤ ringKrullDim (A ⧸ Ideal.span {f}) + 1

theorem polynomial_height_add_coheight_ge (S : Type u_2) [CommRing S] [IsNoetherianRing S] [FiniteRingKrullDim S] (Q : PrimeSpectrum (Polynomial S)) : ↑1 + ringKrullDim S ≤ ↑(Order.height Q + Order.coheight Q)

theorem mvPolynomial_height_add_coheight_ge (k : Type u_2) [Field k] (n : ℕ) (pp : PrimeSpectrum (MvPolynomial (Fin n) k)) : ↑n ≤ Order.height pp + Order.coheight pp

theorem catenary_inequality_polynomial_ring (k : Type u_2) [Field k] (n : ℕ) (p : Ideal (MvPolynomial (Fin n) k)) [p.IsPrime] : ringKrullDim (MvPolynomial (Fin n) k) ≤ ringKrullDim (MvPolynomial (Fin n) k ⧸ p) + ↑p.height

theorem polynomial_ring_dimension_formula (k : Type u_2) [Field k] (n : ℕ) (p : Ideal (MvPolynomial (Fin n) k)) [p.IsPrime] : ↑n ≤ ringKrullDim (MvPolynomial (Fin n) k ⧸ p) + ↑p.height

theorem cor_12_7_dim_irred_component (k : Type u_1) [Field k] (n : ℕ) (_hk : IsAlgClosed k) (m : ℕ) (f : Fin m → MvPolynomial (Fin n) k) (_hhom : ∀ (i : Fin m), ∃ (d : ℕ), 0 < d ∧ ∀ (s : Fin n →₀ ℕ), MvPolynomial.coeff s (f i) ≠ 0 → (s.sum fun (x : Fin n) (e : ℕ) => e) = d) (p : Ideal (MvPolynomial (Fin n) k)) (hp : p ∈ (Ideal.span (Set.range f)).minimalPrimes) : ↑n ≤ ringKrullDim (MvPolynomial (Fin n) k ⧸ p) + ↑↑m

theorem image_castSucc_eq_image {A : Type u_2} {k : ℕ} (f : Fin (k + 1) → A) (j : Fin k) : f ∘ Fin.castSucc '' {i : Fin k | ↑i < ↑j} = f '' {i : Fin (k + 1) | ↑i < ↑j.castSucc}

theorem isRegularSequence_init {A : Type u_2} [CommRing A] {k : ℕ} {f : Fin (k + 1) → A} (hreg : IsRegularSequence f) : IsRegularSequence (f ∘ Fin.castSucc)

def koszulProjL {A : Type u_2} [CommRing A] (b c : ℕ) : (Fin (b + c) → A) →ₗ[A] Fin b → A

def koszulProjR {A : Type u_2} [CommRing A] (b c : ℕ) : (Fin (b + c) → A) →ₗ[A] Fin c → A

def koszulReindex {A : Type u_2} [CommRing A] {a b : ℕ} (h : a = b) : (Fin a → A) →ₗ[A] Fin b → A

def koszulSmulLM {A : Type u_2} [CommRing A] (a_val : A) (k : ℕ) : (Fin k → A) →ₗ[A] Fin k → A

def koszulInjectL {A : Type u_2} [CommRing A] (b c : ℕ) : (Fin b → A) →ₗ[A] Fin (b + c) → A

def koszulInjectR {A : Type u_2} [CommRing A] (b c : ℕ) : (Fin c → A) →ₗ[A] Fin (b + c) → A

noncomputable def koszulDSafe {A : Type u_2} [CommRing A] (n : ℕ) (d' : (i : ℕ) → i < n → (Fin (n.choose (i + 1)) → A) →ₗ[A] Fin (n.choose i) → A) (p : ℕ) : (Fin (n.choose (p + 1)) → A) →ₗ[A] Fin (n.choose p) → A

noncomputable def koszulConeDiff0 {A : Type u_2} [CommRing A] (n : ℕ) (hn : 0 < n) (d' : (i : ℕ) → i < n → (Fin (n.choose (i + 1)) → A) →ₗ[A] Fin (n.choose i) → A) (a : A) : (Fin ((n + 1).choose 1) → A) →ₗ[A] Fin ((n + 1).choose 0) → A

noncomputable def koszulConeDiffSucc {A : Type u_2} [CommRing A] (n p' : ℕ) (hp' : p' < n) (d' : (i : ℕ) → i < n → (Fin (n.choose (i + 1)) → A) →ₗ[A] Fin (n.choose i) → A) (a : A) : (Fin ((n + 1).choose (p' + 2)) → A) →ₗ[A] Fin ((n + 1).choose (p' + 1)) → A

noncomputable def koszulConeDiff {A : Type u_2} [CommRing A] (n : ℕ) (hn : 0 < n) (d' : (i : ℕ) → i < n → (Fin (n.choose (i + 1)) → A) →ₗ[A] Fin (n.choose i) → A) (a : A) (p : ℕ) (hp : p < n + 1) : (Fin ((n + 1).choose (p + 1)) → A) →ₗ[A] Fin ((n + 1).choose p) → A

theorem koszulCone_exactness {A : Type u_2} [CommRing A] {n : ℕ} (hn : 0 < n) (f : Fin (n + 1) → A) (hreg : IsRegularSequence f) (d' : (i : ℕ) → i < n → (Fin (n.choose (i + 1)) → A) →ₗ[A] Fin (n.choose i) → A) (ε' : (Fin (n.choose 0) → A) →ₗ[A] A ⧸ Ideal.span (Set.range (f ∘ Fin.castSucc))) (hε'_surj : Function.Surjective ⇑ε') (hε'_exact : ∀ (hm : 0 < n), ε'.ker = (d' 0 hm).range) (hε'_exact_top : n = 0 → ε'.ker = ⊥) (hd'_exact : ∀ (i : ℕ) (hi : i < n) (hi' : i + 1 < n), (d' i hi).ker = (d' (i + 1) hi').range) (hd'_inj : 0 < n → Function.Injective ⇑(d' (n - 1) ⋯)) (a : A) (ha : a = f (Fin.last n)) : have d := fun (i : ℕ) (hi : i < n + 1) => koszulConeDiff n hn d' a i hi; have h_choose0 := ⋯; have ε := { toFun := fun (v : Fin ((n + 1).choose 0) → A) => (Ideal.Quotient.mk (Ideal.span (Set.range f))) (v ⟨0, h_choose0⟩), map_add' := ⋯, map_smul' := ⋯ }; (∀ (hm : 0 < n + 1), ε.ker = (d 0 hm).range) ∧ (∀ (i : ℕ) (hi : i < n + 1) (hi' : i + 1 < n + 1), (d i hi).ker = (d (i + 1) hi').range) ∧ (0 < n + 1 → Function.Injective ⇑(d (n + 1 - 1) ⋯))

theorem lemma_12_8_koszul_exact {A : Type u_2} [CommRing A] {m : ℕ} (f : Fin m → A) (hreg : IsRegularSequence f) : ∃ (d : (i : ℕ) → i < m → (Fin (m.choose (i + 1)) → A) →ₗ[A] Fin (m.choose i) → A) (ε : (Fin (m.choose 0) → A) →ₗ[A] A ⧸ Ideal.span (Set.range f)), Function.Surjective ⇑ε ∧ (∀ (hm : 0 < m), ε.ker = (d 0 hm).range) ∧ (m = 0 → ε.ker = ⊥) ∧ (∀ (i : ℕ) (hi : i < m) (hi' : i + 1 < m), (d i hi).ker = (d (i + 1) hi').range) ∧ ∀ (hm : 0 < m), Function.Injective ⇑(d (m - 1) ⋯)

theorem X_nonzerodiv_mod_lower (k : Type u_2) [Field k] (n : ℕ) (j : Fin n) (p : MvPolynomial (Fin n) k) (hp : MvPolynomial.X j * p ∈ Ideal.span (MvPolynomial.X '' {i : Fin n | ↑i < ↑j})) : p ∈ Ideal.span (MvPolynomial.X '' {i : Fin n | ↑i < ↑j})

theorem variables_form_regular_sequence (k : Type u_2) [Field k] (n : ℕ) : IsRegularSequence fun (i : Fin n) => MvPolynomial.X i

theorem koszul_complex_is_acyclic (k : Type u_2) [Field k] (n : ℕ) : ∃ (r : Fin (n + 1) → ℕ) (d : (i : ℕ) → (x : i < n) → (Fin (r ⟨i + 1, ⋯⟩) → MvPolynomial (Fin n) k) →ₗ[MvPolynomial (Fin n) k] Fin (r ⟨i, ⋯⟩) → MvPolynomial (Fin n) k), (∀ (i : ℕ) (hi : i < n) (hi' : i + 1 < n), d i hi ∘ₗ d (i + 1) hi' = 0) ∧ (∀ (i : ℕ) (hi : i < n) (hi' : i + 1 < n), (d i hi).ker = (d (i + 1) hi').range) ∧ (∀ (hn : 0 < n), Function.Injective ⇑(d (n - 1) ⋯)) ∧ ∀ (p : ℕ) (hp : p ≤ n), r ⟨p, ⋯⟩ = n.choose p

theorem eval_zero_of_homogeneous_pos_deg (k : Type u_1) [Field k] (n : ℕ) (f : MvPolynomial (Fin n) k) (d : ℕ) (hd : 0 < d) (hhom : ∀ (m : Fin n →₀ ℕ), MvPolynomial.coeff m f ≠ 0 → (m.sum fun (x : Fin n) (e : ℕ) => e) = d) : (MvPolynomial.eval 0) f = 0

theorem assocPrimes_quotient_subset_minimalPrimes_polynomial (k : Type u_2) [inst : Field k] (n : ℕ) (I p : Ideal (MvPolynomial (Fin n) k)) (hp : p ∈ associatedPrimes (MvPolynomial (Fin n) k) (MvPolynomial (Fin n) k ⧸ I)) : p ∈ I.minimalPrimes

theorem height_le_of_assocPrime_quotient_span_range (k : Type u_2) [Field k] (n m : ℕ) (f : Fin m → MvPolynomial (Fin n) k) (p : Ideal (MvPolynomial (Fin n) k)) (hp : p ∈ associatedPrimes (MvPolynomial (Fin n) k) (MvPolynomial (Fin n) k ⧸ Ideal.span (Set.range f))) : p.height ≤ ↑m

theorem assoc_prime_dim_lower_bound (k : Type u_2) [Field k] (n : ℕ) (_hk : IsAlgClosed k) (f : Fin n → MvPolynomial (Fin n) k) (_hhom : ∀ (i : Fin n), ∃ (d : ℕ), 0 < d ∧ ∀ (m : Fin n →₀ ℕ), MvPolynomial.coeff m (f i) ≠ 0 → (m.sum fun (x : Fin n) (e : ℕ) => e) = d) (j : Fin n) (p : Ideal (MvPolynomial (Fin n) k)) (hp : p ∈ associatedPrimes (MvPolynomial (Fin n) k) (MvPolynomial (Fin n) k ⧸ Ideal.span (f '' {i : Fin n | ↑i < ↑j}))) : ↑(↑n - ↑↑j) ≤ ringKrullDim (MvPolynomial (Fin n) k ⧸ p)

theorem reverse_catenary_polynomial_ring (k : Type u_2) [Field k] (n : ℕ) (p : Ideal (MvPolynomial (Fin n) k)) [p.IsPrime] : ringKrullDim (MvPolynomial (Fin n) k ⧸ p) + ↑p.height ≤ ↑n

theorem quotient_dim_bound_from_vanishing (k : Type u_2) [Field k] (n : ℕ) (hk : IsAlgClosed k) (f : Fin n → MvPolynomial (Fin n) k) (hhom : ∀ (i : Fin n), ∃ (d : ℕ), 0 < d ∧ ∀ (m : Fin n →₀ ℕ), MvPolynomial.coeff m (f i) ≠ 0 → (m.sum fun (x : Fin n) (e : ℕ) => e) = d) (hvanish : ∀ (v : Fin n → k), (∀ (i : Fin n), (MvPolynomial.eval v) (f i) = 0) → v = 0) (j : Fin n) (p : Ideal (MvPolynomial (Fin n) k)) [p.IsPrime] (hp_contains : ∀ (i : Fin n), ↑i ≤ ↑j → f i ∈ p) : ringKrullDim (MvPolynomial (Fin n) k ⧸ p) + ↑(↑j + 1) ≤ ↑n

theorem height_bound_from_dim_bounds (dim : WithBot ℕ∞) (ht : ℕ∞) (n j1 : ℕ) (h_le : dim + ↑ht ≤ ↑n) (h_ge : ↑n ≤ dim + ↑ht) (h_dim : dim + ↑j1 ≤ ↑n) : ↑j1 ≤ ht

theorem height_ge_succ_of_vanishing_contains (k : Type u_2) [Field k] (n : ℕ) (hk : IsAlgClosed k) (f : Fin n → MvPolynomial (Fin n) k) (hhom : ∀ (i : Fin n), ∃ (d : ℕ), 0 < d ∧ ∀ (m : Fin n →₀ ℕ), MvPolynomial.coeff m (f i) ≠ 0 → (m.sum fun (x : Fin n) (e : ℕ) => e) = d) (hvanish : ∀ (v : Fin n → k), (∀ (i : Fin n), (MvPolynomial.eval v) (f i) = 0) → v = 0) (j : Fin n) (p : Ideal (MvPolynomial (Fin n) k)) [p.IsPrime] (hp_contains : ∀ (i : Fin n), ↑i ≤ ↑j → f i ∈ p) : ↑↑j + 1 ≤ p.height

theorem prime_dim_upper_bound_from_vanishing (k : Type u_2) [Field k] (n : ℕ) (hk : IsAlgClosed k) (f : Fin n → MvPolynomial (Fin n) k) (hhom : ∀ (i : Fin n), ∃ (d : ℕ), 0 < d ∧ ∀ (m : Fin n →₀ ℕ), MvPolynomial.coeff m (f i) ≠ 0 → (m.sum fun (x : Fin n) (e : ℕ) => e) = d) (hvanish : ∀ (v : Fin n → k), (∀ (i : Fin n), (MvPolynomial.eval v) (f i) = 0) → v = 0) (j : Fin n) (p : Ideal (MvPolynomial (Fin n) k)) [p.IsPrime] (hp_contains : ∀ (i : Fin n), ↑i ≤ ↑j → f i ∈ p) : ringKrullDim (MvPolynomial (Fin n) k ⧸ p) + ↑(↑↑j + 1) ≤ ↑n

theorem fj_not_in_associated_prime (k : Type u_2) [Field k] (n : ℕ) (hk : IsAlgClosed k) (f : Fin n → MvPolynomial (Fin n) k) (hhom : ∀ (i : Fin n), ∃ (d : ℕ), 0 < d ∧ ∀ (m : Fin n →₀ ℕ), MvPolynomial.coeff m (f i) ≠ 0 → (m.sum fun (x : Fin n) (e : ℕ) => e) = d) (hvanish : ∀ (v : Fin n → k), (∀ (i : Fin n), (MvPolynomial.eval v) (f i) = 0) → v = 0) (j : Fin n) (p : Ideal (MvPolynomial (Fin n) k)) (hp : p ∈ associatedPrimes (MvPolynomial (Fin n) k) (MvPolynomial (Fin n) k ⧸ Ideal.span (f '' {i : Fin n | ↑i < ↑j}))) : f j ∉ p

theorem prop_12_9_non_zero_divisor_step (k : Type u_1) [Field k] (n : ℕ) (hk : IsAlgClosed k) (f : Fin n → MvPolynomial (Fin n) k) (hhom : ∀ (i : Fin n), ∃ (d : ℕ), 0 < d ∧ ∀ (m : Fin n →₀ ℕ), MvPolynomial.coeff m (f i) ≠ 0 → (m.sum fun (x : Fin n) (e : ℕ) => e) = d) (hvanish : ∀ (v : Fin n → k), (∀ (i : Fin n), (MvPolynomial.eval v) (f i) = 0) → v = 0) (j : Fin n) (r : MvPolynomial (Fin n) k ⧸ Ideal.span (f '' {i : Fin n | ↑i < ↑j})) (hr : r ≠ 0) : (Ideal.Quotient.mk (Ideal.span (f '' {i : Fin n | ↑i < ↑j}))) (f j) • r ≠ 0

theorem prop_12_9_regular_sequence (k : Type u_1) [Field k] (n : ℕ) (hk : IsAlgClosed k) (f : Fin n → MvPolynomial (Fin n) k) (hhom : ∀ (i : Fin n), ∃ (d : ℕ), 0 < d ∧ ∀ (m : Fin n →₀ ℕ), MvPolynomial.coeff m (f i) ≠ 0 → (m.sum fun (x : Fin n) (e : ℕ) => e) = d) (hvanish : ∀ (v : Fin n → k), (∀ (i : Fin n), (MvPolynomial.eval v) (f i) = 0) → v = 0) : IsRegularSequence f

noncomputable def quotientHomogeneousSubmodule (k : Type u_1) [Field k] (n : ℕ) (I : Ideal (MvPolynomial (Fin n) k)) (i : ℕ) : Submodule k (MvPolynomial (Fin n) k ⧸ I)

def qAnalog (d : ℕ) : PowerSeries ℤ

def invOneSubX : PowerSeries ℤ

theorem mem_finsuppAntidiag_univ_iff_degree' {n d : ℕ} (f : Fin n →₀ ℕ) : f ∈ Finset.univ.finsuppAntidiag d ↔ Finsupp.degree f = d

@[implicit_reducible]

noncomputable instance fintypeFinsuppDegreeEq' {n : ℕ} (d : ℕ) : Fintype ↑{s : Fin n →₀ ℕ | Finsupp.degree s = d}

theorem finrank_homogeneousSubmodule_eq' (k : Type u_1) [Field k] {n : ℕ} (d : ℕ) : Module.finrank k ↥(MvPolynomial.homogeneousSubmodule (Fin n) k d) = n.multichoose d

theorem hilbert_series_polynomial_ring (k : Type u_1) [Field k] (n : ℕ) : hilbertSeries (MvPolynomial.homogeneousSubmodule (Fin n) k) = invOneSubX ^ n

theorem hilbert_series_quotient_regular_seq (k : Type u_1) [Field k] (n m : ℕ) (s : Fin m → MvPolynomial (Fin n) k) (degs : Fin m → ℕ) (hhom : ∀ (i : Fin m) (c : Fin n →₀ ℕ), MvPolynomial.coeff c (s i) ≠ 0 → (c.sum fun (x : Fin n) (e : ℕ) => e) = degs i) (hreg : IsRegularSequence s) : hilbertSeries (quotientHomogeneousSubmodule k n (Ideal.span (Set.range s))) = (∏ i : Fin m, (1 - PowerSeries.X ^ degs i)) * hilbertSeries (MvPolynomial.homogeneousSubmodule (Fin n) k)

theorem one_sub_X_pow_mul_invOneSubX (d : ℕ) : (1 - PowerSeries.X ^ d) * invOneSubX = qAnalog d

theorem prod_one_sub_mul_invOneSubX_eq_prod_qAnalog {m : ℕ} (d : Fin m → ℕ) : (∏ i : Fin m, (1 - PowerSeries.X ^ d i)) * invOneSubX ^ m = ∏ i : Fin m, qAnalog (d i)

theorem free_over_adjoin_of_homogeneous (k : Type u_2) [Field k] (n : ℕ) (f : Fin n → MvPolynomial (Fin n) k) (d : Fin n → ℕ) (hd : ∀ (i : Fin n), 0 < d i) (hhom : ∀ (i : Fin n) (m : Fin n →₀ ℕ), MvPolynomial.coeff m (f i) ≠ 0 → (m.sum fun (x : Fin n) (e : ℕ) => e) = d i) (hfin : Module.Finite (↥(Algebra.adjoin k (Set.range f))) (MvPolynomial (Fin n) k)) : Module.Free (↥(Algebra.adjoin k (Set.range f))) (MvPolynomial (Fin n) k)

theorem rank_eq_prod_of_homogeneous (k : Type u_2) [Field k] (n : ℕ) (f : Fin n → MvPolynomial (Fin n) k) (d : Fin n → ℕ) (hd : ∀ (i : Fin n), 0 < d i) (hhom : ∀ (i : Fin n) (m : Fin n →₀ ℕ), MvPolynomial.coeff m (f i) ≠ 0 → (m.sum fun (x : Fin n) (e : ℕ) => e) = d i) (hfin : Module.Finite (↥(Algebra.adjoin k (Set.range f))) (MvPolynomial (Fin n) k)) : Module.rank (↥(Algebra.adjoin k (Set.range f))) (MvPolynomial (Fin n) k) = ↑(Finset.univ.prod d)

theorem filtered_deformation_iso (k : Type u_2) [Field k] (n : ℕ) (f : Fin n → MvPolynomial (Fin n) k) (d : Fin n → ℕ) (hd : ∀ (i : Fin n), 0 < d i) (hhom : ∀ (i : Fin n) (m : Fin n →₀ ℕ), MvPolynomial.coeff m (f i) ≠ 0 → (m.sum fun (x : Fin n) (e : ℕ) => e) = d i) (hfin : Module.Finite (↥(Algebra.adjoin k (Set.range f))) (MvPolynomial (Fin n) k)) : Nonempty (MvPolynomial (Fin n) k ≃ₗ[↥(Algebra.adjoin k (Set.range f))] Fin (Finset.univ.prod d) → ↥(Algebra.adjoin k (Set.range f)))

theorem prop_12_10_free_module (k : Type u_1) [Field k] (n : ℕ) (f : Fin n → MvPolynomial (Fin n) k) (d : Fin n → ℕ) (hd : ∀ (i : Fin n), 0 < d i) (hhom : ∀ (i : Fin n) (m : Fin n →₀ ℕ), MvPolynomial.coeff m (f i) ≠ 0 → (m.sum fun (x : Fin n) (e : ℕ) => e) = d i) (hfin : Module.Finite (↥(Algebra.adjoin k (Set.range f))) (MvPolynomial (Fin n) k)) : Module.Free (↥(Algebra.adjoin k (Set.range f))) (MvPolynomial (Fin n) k) ∧ Module.finrank (↥(Algebra.adjoin k (Set.range f))) (MvPolynomial (Fin n) k) = Finset.univ.prod d

theorem prop_12_10_hilbert_series (k : Type u_1) [Field k] (n : ℕ) (hk : IsAlgClosed k) (f : Fin n → MvPolynomial (Fin n) k) (d : Fin n → ℕ) (hd : ∀ (i : Fin n), 0 < d i) (hhom : ∀ (i : Fin n) (m : Fin n →₀ ℕ), MvPolynomial.coeff m (f i) ≠ 0 → (m.sum fun (x : Fin n) (e : ℕ) => e) = d i) (hvanish : ∀ (v : Fin n → k), (∀ (i : Fin n), (MvPolynomial.eval v) (f i) = 0) → v = 0) (_hfin : Module.Finite (↥(Algebra.adjoin k (Set.range f))) (MvPolynomial (Fin n) k)) : hilbertSeries (quotientHomogeneousSubmodule k n (Ideal.span (Set.range f))) = ∏ i : Fin n, qAnalog (d i)