Module

SignPolynomialInvariants.lean

Nyll.SchemeTheory.RingTheory.SignPolynomialInvariants

5 declarations indexed from sourceView source ↗

Module documentation

Invariants of simultaneous sign change

Over every field of characteristic different from two, the invariants of simultaneous sign change are exactly the subalgebra generated by X i * X j. There is no restriction on the number of variables in this algebraic statement. The normalization cover, its generic degree, and its ramification locus are separate assertions of Stacks Project, Tag 0BTE.

Imports10

Nyll.SchemeTheory.RingTheory.SignPolynomialAction
Nyll.SchemeTheory.RingTheory.SignPolynomialMonomials
Mathlib.Algebra.MvPolynomial.Basic
Mathlib.Algebra.MvPolynomial.Eval
Mathlib.Algebra.Algebra.Subalgebra.Lattice
Mathlib.Data.Finsupp.Weight
Mathlib.Algebra.Field.Basic
Mathlib.Algebra.Ring.Commute
Mathlib.Algebra.Ring.Parity
Mathlib.Algebra.BigOperators.Group.Finset.Basic

Imported by2

theorem

simultaneousNeg_monomial

L39 ↗

SchemeTheory.SignPolynomial.simultaneousNeg_monomial

Documentation

Sign change acts on a monomial by the parity of its total exponent.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
open scoped BigOperators
section Coefficients
variable (k : Type*) [CommRing k] (n : ℕ)

Lean source · statement

theorem simultaneousNeg_monomial (d : Fin n →₀ ℕ) (c : k) :
    simultaneousNeg k n (monomial d c) = monomial d ((-1 : k) ^ d.degree * c)

theorem

coeff_simultaneousNeg

L57 ↗

SchemeTheory.SignPolynomial.coeff_simultaneousNeg

Documentation

The actual coefficient formula for the simultaneous sign involution.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
open scoped BigOperators
section Coefficients
variable (k : Type*) [CommRing k] (n : ℕ)

Lean source · statement

theorem coeff_simultaneousNeg (p : MvPolynomial (Fin n) k) (d : Fin n →₀ ℕ) :
    (simultaneousNeg k n p).coeff d = (-1 : k) ^ d.degree * p.coeff d

theorem

mem_fixedSubalgebra_iff_even_support

L79 ↗

SchemeTheory.SignPolynomial.mem_fixedSubalgebra_iff_even_support

Documentation

Invariants have precisely even exponents at their nonzero coefficients.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
open scoped BigOperators
section Invariants
variable (k : Type*) [Field k] (n : ℕ) (htwo : (2 : k) ≠ 0)
include htwo

Lean source · statement

theorem mem_fixedSubalgebra_iff_even_support (p : MvPolynomial (Fin n) k) :
    p ∈ fixedSubalgebra k n ↔ ∀ d : Fin n →₀ ℕ, p.coeff d ≠ 0 → Even d.degree

theorem

fixedSubalgebra_eq_quadraticSubalgebra

L105 ↗

SchemeTheory.SignPolynomial.fixedSubalgebra_eq_quadraticSubalgebra

Documentation

The literal invariant-ring calculation for the sign quotient in Tag 0BTE.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
open scoped BigOperators
section Invariants
variable (k : Type*) [Field k] (n : ℕ) (htwo : (2 : k) ≠ 0)
include htwo

Lean source · statement

theorem fixedSubalgebra_eq_quadraticSubalgebra :
    fixedSubalgebra k n = quadraticSubalgebra k n

theorem

forall_signAction_iff_mem_quadraticSubalgebra

L122 ↗

SchemeTheory.SignPolynomial.forall_signAction_iff_mem_quadraticSubalgebra

Documentation

An action-form endpoint for the original polynomial ring, with no invariant-ring hypothesis.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
open scoped BigOperators
section Invariants
variable (k : Type*) [Field k] (n : ℕ) (htwo : (2 : k) ≠ 0)
include htwo

Lean source · statement

theorem forall_signAction_iff_mem_quadraticSubalgebra (p : MvPolynomial (Fin n) k) :
    (∀ ε : ℤˣ, (signAction k n).smul ε p = p) ↔ p ∈ quadraticSubalgebra k n

Module documentation

Invariants of simultaneous sign change

Declarations

simultaneousNeg_monomial

coeff_simultaneousNeg

mem_fixedSubalgebra_iff_even_support

fixedSubalgebra_eq_quadraticSubalgebra

forall_signAction_iff_mem_quadraticSubalgebra