Documentation

TauCeti.Geometry.RealAlgebraic.Stack.Lazard.Product

Lazard delineations of products #

A Lazard delineation of a nonzero finite product over a preconnected base induces a Lazard delineation of its factors with exactly the same ordered root functions. Conversely, a Lazard delineation of a finite family with nonzero product is one of the product, over any base. No preservation of ordinary fiber degrees or nonnullification is needed. Factors may share roots and have repeated roots; the empty family is included.

Constant product valuation passes to each divisor along continuous sections. On each product root section this fixes the factor's root multiplicity. On a continuous graph in a sector it fixes the factor's removed base exponents. Multiplicativity of Lazard evaluation supplies root coverage and ensures that each section is used by a factor.

This is the product-to-family step in Lazard lifting: a single-polynomial delineability theorem applied to a basis product provides the common stack for the basis, even over nullified ordinary fibers. Its section and sector valuations follow from the existing LazardDelineation API. The converse direction is a direct consequence of multiplicativity: removed base exponents and root multiplicities of the product are the sums of those of its factors. It lifts a polynomial divisible by the distinguished variable from the lifting of its cofactor.

Main declarations #

References #

source
noncomputable def TauCeti.LazardDelineation.ofProd {ι : Type u_1} [Fintype ι] {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation (fun (x : Unit) => ∏ k : ι, F k) S) (hS : IsPreconnected S) (hprod : ∏ k : ι, F k ≠ 0) :
LazardDelineation F S

Recover a common Lazard delineation of the factors from a delineation of their nonzero product over a preconnected base. The root list is unchanged. Ordinary fibers may be nullified, and neither their degrees nor the degrees of Lazard evaluations need to be constant.

Instances For
    source
    @[simp]
    theorem TauCeti.LazardDelineation.ofProd_count {ι : Type u_1} [Fintype ι] {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation (fun (x : Unit) => ∏ k : ι, F k) S) (hS : IsPreconnected S) (hprod : ∏ k : ι, F k ≠ 0) :
    (D.ofProd hS hprod).count = D.count

    Recovering the factors' Lazard delineation preserves the number of root sections.

    source
    @[simp]
    theorem TauCeti.LazardDelineation.ofProd_root {ι : Type u_1} [Fintype ι] {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation (fun (x : Unit) => ∏ k : ι, F k) S) (hS : IsPreconnected S) (hprod : ∏ k : ι, F k ≠ 0) (i : Fin (D.ofProd hS hprod).count) (x : ↑S) :
    (D.ofProd hS hprod).root i x = D.root (Fin.cast ⋯ i) x

    Recovering the factors' Lazard delineation preserves the ordered root functions.

    source
    noncomputable def TauCeti.LazardDelineation.prod {ι : Type u_1} [Fintype ι] {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) (hprod : ∏ k : ι, F k ≠ 0) :
    LazardDelineation (fun (x : Unit) => ∏ k : ι, F k) S

    A Lazard delineation of a finite family with nonzero product is a Lazard delineation of the product, with the same ordered root functions. Its removed base exponents and its root multiplicities are the sums of those of the factors. No connectedness of the base is needed.

    Instances For
      source
      @[simp]
      theorem TauCeti.LazardDelineation.prod_count {ι : Type u_1} [Fintype ι] {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) (hprod : ∏ k : ι, F k ≠ 0) :
      (D.prod hprod).count = D.count

      Passing to the product preserves the number of root sections.

      source
      @[simp]
      theorem TauCeti.LazardDelineation.prod_root {ι : Type u_1} [Fintype ι] {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) (hprod : ∏ k : ι, F k ≠ 0) (i : Fin (D.prod hprod).count) (x : ↑S) :
      (D.prod hprod).root i x = D.root (Fin.cast ⋯ i) x

      Passing to the product preserves the ordered root functions.

      source
      @[simp]
      theorem TauCeti.LazardDelineation.prod_exponent {ι : Type u_1} [Fintype ι] {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) (hprod : ∏ k : ι, F k ≠ 0) (u : Unit) :
      (D.prod hprod).exponent u = ∑ k : ι, D.exponent k

      The removed base exponents of the product are the sum of those of the factors.

      source
      @[simp]
      theorem TauCeti.LazardDelineation.prod_multiplicity {ι : Type u_1} [Fintype ι] {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) (hprod : ∏ k : ι, F k ≠ 0) (u : Unit) (i : Fin (D.prod hprod).count) :
      (D.prod hprod).multiplicity u i = ∑ k : ι, D.multiplicity k (Fin.cast ⋯ i)

      The multiplicity of a root function in the product is the sum of its multiplicities in the factors.