Mixed cut flags with injective cuts and reduced final quotients after completion

Open

PhilipponMultiplicity.exists_mixed_cut_flag_with_completed_local_conditions

by tomasz · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrycommutative-algebraphilippon-multiplicityproof-frontier

Let $W$ be a nonempty irreducible closed subset of $M=\prod_i\mathbf P^{n_i}$ over a Philippon base field $K$ . Let $\alpha=(\alpha_i)$ satisfy $0\leq\alpha_i\leq n_i$ and $\sum_i\alpha_i=\dim W$ . If $B\subseteq W$ is closed and $W\setminus B$ is nonempty, there is a product linear section $L$ of block codimensions $\alpha_i$ whose intersection with $W$ is finite and disjoint from $B$ .

The section can be defined by an ordered list of block-linear forms $P_0,\ldots,P_{s-1}$ , with exactly $\alpha_i$ forms from block $i$ . Write $A$ for the multicone polynomial coordinate ring and put $J_0=I(W)$ and $J_{k+1}=J_k+(P_k)$ . These equations define exactly the indicated section on multiprojective points.

For a coordinate tuple $v$ with every block nonzero, put $R_v=A_{\mathfrak m_v}$ , where $\mathfrak m_v$ is its evaluation maximal ideal, and let $\widehat R_v$ be its maximal-ideal-adic completion. Writing $V(J)$ for the affine zero set of $J$ , the local conclusions are

v\in V(J_k)\ \Longrightarrow \bigl(\cdot P_k:\widehat R_v/J_k\widehat R_v\longrightarrow \widehat R_v/J_k\widehat R_v\bigr)\text{ is injective},\qquad k<s,

and

v\in V(J_s)\ \Longrightarrow\ J_s\widehat R_v\text{ is radical}.

These completed local conditions supply the geometric input for recovering the ordinary point-local conditions by faithful flatness.

Formalization Note. The accepted reduction proves the passage from ordinary local injective cuts and regular final local quotients to these completed local conditions. Its sole remaining Open input is the geometric mixed-flag construction with regular final local quotients. Noetherianity of local completion is now Proved by power-series evaluation and adic lifting. Quotient flatness, ascent of multiplication injectivity, local regularity ascent, and the implication from regularity to radicality are proved in the reduction. All hypotheses, witnesses, and the original formal statement are unchanged.

Preamble

import Mathlib.RingTheory.AdicCompletion.LocalRing
import Mathlib.RingTheory.Nullstellensatz
import Mathlib.RingTheory.Localization.Ideal
import Definitions.Def_PhilipponMultiplicity_GeometricSupport
set_option autoImplicit false
open scoped BigOperators Topology

Formal statement

namespace PhilipponMultiplicity
open SectionThree SectionThreeSupport

theorem exists_mixed_cut_flag_with_completed_local_conditions
    (K : Type*) [NontriviallyNormedField K] (hK : IsPhilipponBaseField K) :
    ∀ (M : MultiProjectiveSpace K) (W : Set M.Point),
      @IsClosed _ M.zariskiTopology W → @IsIrreducible _ M.zariskiTopology W →
      ∀ (α : M.FactorIndex → ℕ), (∀ i, α i ≤ M.ambientDimension i) →
      (∑ i, α i = locusDimension M W) →
      ∀ B : Set M.Point, @IsClosed _ M.zariskiTopology B → B ⊆ W →
      (W \ B).Nonempty →
      ∃ L : ∀ i : M.FactorIndex, Submodule K (Fin (M.ambientDimension i + 1) → K),
        (∀ i, Module.finrank K (L i) + α i = M.ambientDimension i + 1) ∧
        (linearSlice M W L).Finite ∧ Disjoint (linearSlice M W L) B ∧
        ∃ (l : List M.FactorIndex) (P : ℕ → M.CoordinateRing)
          (J : ℕ → Ideal M.CoordinateRing),
          (∀ i, l.count i = α i) ∧ J 0 = M.vanishingIdeal W ∧
          (∀ k (hk : k < l.length),
            M.IsHomogeneous (P k) (Pi.single l[k] 1) ∧
            J (k+1) = J k ⊔ Ideal.span {P k} ∧
            ∀ v : M.Variable → K,
              (∀ i : M.FactorIndex,
                (fun j : Fin (M.ambientDimension i + 1) => v ⟨i,j⟩) ≠ 0) →
              (∀ Q ∈ J k, MvPolynomial.eval v Q = 0) →
              let R := Localization.AtPrime (MvPolynomial.vanishingIdeal K {v})
              let C := AdicCompletion (IsLocalRing.maximalIdeal R) R
              let f := (algebraMap R C).comp (algebraMap M.CoordinateRing R)
              ∀ Q : C, f (P k) * Q ∈ (J k).map f → Q ∈ (J k).map f) ∧
          (∀ x : M.Point, x ∈ linearSlice M W L ↔
            x ∈ W ∧ ∀ k < l.length, M.eval (P k) x = 0) ∧
          (∀ v : M.Variable → K,
            (∀ i : M.FactorIndex,
              (fun j : Fin (M.ambientDimension i + 1) => v ⟨i,j⟩) ≠ 0) →
            (∀ Q ∈ J l.length, MvPolynomial.eval v Q = 0) →
            let R := Localization.AtPrime (MvPolynomial.vanishingIdeal K {v})
            let C := AdicCompletion (IsLocalRing.maximalIdeal R) R
            let f := (algebraMap R C).comp (algebraMap M.CoordinateRing R)
            ((J l.length).map f).IsRadical) := by sorry

end PhilipponMultiplicity

Source

Philippon, Lemmes de zeros dans les groupes algebriques commutatifs, Bulletin de la SMF 114 (1986), Lemma 3.1 and the mixed-section paragraph, pp.363–364, https://numdam.org/articles/10.24033/bsmf.2060/ . Nguyen Tien Manh and Duong Quoc Viet, Filter-regular sequences and mixed multiplicities, arXiv:0901.3825v1, Definition 2.1 p.3, notes (i)–(ii) p.4, Proposition 2.6 p.6, https://arxiv.org/abs/0901.3825 . S. L. Kleiman, The transversality of a general translate, Compositio Mathematica 28 (1974), Theorem 2 p.290 and Corollary 4 p.291, https://numdam.org/item/CM_1974__28_3_287_0/ . Stacks Project, Lemma 10.97.3 (tag 00MC), https://stacks.math.columbia.edu/tag/00MC . Auxiliary synthesis: generic filter-regular flags and transversality on the smooth open are the intended geometric inputs. The completed local construction remains Open. Faithful flatness supplies the separate checked descent to the original point-local conditions; radicality ascent for arbitrary Noetherian rings is not asserted.

View graph