General mixed linear section avoiding a proper closed boundary

Open

PhilipponMultiplicity.generic_mixed_linear_section_avoiding_boundary

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

intersection-theorymixed-degreesphilippon-multiplicityproof-frontier

Let $W$ be a closed irreducible subvariety of a product of projective spaces over a Philippon base field, and let $B\subset W$ be a proper closed subset. For an admissible mixed index $\alpha$ with $\sum_i\alpha_i=\dim W$ , there is a finite intersection $Z=W\cap\prod_iL_i$ , where $L_i$ has codimension $\alpha_i$ , such that $Z\cap B=\varnothing$ and

\mathcal H(Z;1,\ldots,1)=c_\alpha(I(W)).

An accepted proof-sketch proves the Hilbert-polynomial computation and reduces the theorem to the refexistence of a filter-regular mixed linear flag with reduced final ideal. That geometric child remains Open. The checked algebra identifies Hilbert polynomials from eventual homogeneous-piece equality, applies the colon exact sequence to each cut, and proves that iterated mixed finite differences extract the top coefficient with the exact product-of-factorials normalization. Zero coefficients and empty final sections are allowed.

Source: Philippon (1986), pp. 363–364, Lemma 3.1 and the general-section interpretation before Lemma 3.2. The formal statement is unchanged.

Preamble

import Definitions.Def_PhilipponMultiplicity_GeometricSupport
set_option autoImplicit false
open scoped BigOperators Topology

Formal statement

namespace PhilipponMultiplicity
open SectionThree

theorem generic_mixed_linear_section_avoiding_boundary
    (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 ∧
        locusDegreeValue M (linearSlice M W L) (fun _ => 1) =
          idealMixedDegree M (M.vanishingIdeal W) α := by sorry

end PhilipponMultiplicity

Source

Philippon (1986), p. 364, the paragraph preceding Lemma 3.2: computation of the mixed Hilbert coefficient by general linear subspaces; see also the mixed-degree definition on p. 359. https://numdam.org/articles/10.24033/bsmf.2060/ . The proper-closed-boundary avoidance is the explicit genericity refinement needed for the mission’s locally closed formulation and remains Open.

View graph