Hypersurface section of a homogeneous prime

This file implements blueprint node B01 of the algebra backend: for a homogeneous prime Q of P = MvPolynomial σ K and a form G ∉ Q of degree e,

homHilbert (Q ⊔ (G)) t + homHilbert Q (t - e) = homHilbert Q t for e ≤ t.

Multiplication by the class gbar of G is an injective K-linear map of the domain P ⧸ Q (Q is prime and G ∉ Q) sending the image V_{t-e} of P_{t-e} into the image V_t of P_t; its image is exactly the kernel of the factor map V_t → P ⧸ (Q ⊔ (G)) (ker_factor_inf_map_eq_map_mulLeft): a form F of degree t in Q ⊔ (G) is q + u * G, and taking degree-t homogeneous components gives F = q_t + u_{t-e} * G with q_t ∈ Q. Rank–nullity for the factor map restricted to V_t then gives the identity.

Main declarations

• Nikodym.LowerBound.ker_factor_inf_map_eq_map_mulLeft: the kernel computation.
• Nikodym.LowerBound.homHilbert_sup_span_singleton_add: the identity above (blueprint B01).

theorem Nikodym.LowerBound.ker_factor_inf_map_eq_map_mulLeft {K : Type u_1} [Field K] {σ : Type u_2} {Q : Ideal (MvPolynomial σ K)} (hQ : Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule σ K) Q) {G : MvPolynomial σ K} {e : ℕ} (hG : G.IsHomogeneous e) {t : ℕ} (ht : e ≤ t) : (Ideal.Quotient.factorₐ K ⋯).toLinearMap.ker ⊓ Submodule.map (Ideal.Quotient.mkₐ K Q).toLinearMap (MvPolynomial.homogeneousSubmodule σ K t) = Submodule.map (LinearMap.mulLeft K ((Ideal.Quotient.mk Q) G)) (Submodule.map (Ideal.Quotient.mkₐ K Q).toLinearMap (MvPolynomial.homogeneousSubmodule σ K (t - e)))

Blueprint B01, kernel computation: for a homogeneous ideal Q, a form G of degree e ≤ t, the part of the image V_t of P_t in P ⧸ Q killed by the factor map P ⧸ Q → P ⧸ (Q ⊔ (G)) is gbar • V_{t-e}, the image of V_{t-e} under multiplication by the class of G.

theorem Nikodym.LowerBound.homHilbert_sup_span_singleton_add {K : Type u_1} [Field K] {σ : Type u_2} [Finite σ] {Q : Ideal (MvPolynomial σ K)} [Q.IsPrime] (hQ : Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule σ K) Q) {G : MvPolynomial σ K} {e : ℕ} (hG : G.IsHomogeneous e) (hGQ : G ∉ Q) {t : ℕ} (ht : e ≤ t) : homHilbert (Q ⊔ Ideal.span {G}) t + homHilbert Q (t - e) = homHilbert Q t

Blueprint B01: hypersurface section. For a homogeneous prime Q of MvPolynomial σ K and a form G ∉ Q of degree e ≤ t, homHilbert (Q ⊔ (G)) t + homHilbert Q (t - e) = homHilbert Q t. Multiplication by the class of G embeds P_{t-e} ⧸ Q_{t-e} into P_t ⧸ Q_t with image the kernel of the surjection onto P_t ⧸ (Q ⊔ (G))_t.