Module

SignPolynomialFinite.lean

Nyll.SchemeTheory.RingTheory.SignPolynomialFinite

5 declarations indexed from sourceView source ↗

Module documentation

Finiteness of the simultaneous sign quotient

The polynomial ring is finite over its concrete quadratic subalgebra. The invariant-ring input is the proved calculation for simultaneous sign change, with the action explicitly selected. These statements allow zero variables.

Imports5

Nyll.SchemeTheory.RingTheory.SignPolynomialInvariants
Mathlib.RingTheory.Invariant.Basic
Mathlib.RingTheory.FiniteType
Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Mathlib.Algebra.GroupWithZero.Units.Fintype

Imported by3

theorem

quadratic_finiteType

L29 ↗

SchemeTheory.SignPolynomial.quadratic_finiteType

Documentation

The actual quadratic subalgebra has finite type over the coefficient field.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [Field k] (n : ℕ)

Lean source · statement

theorem quadratic_finiteType : Algebra.FiniteType k (quadraticSubalgebra k n)

theorem

polynomial_finiteType_quadratic

L34 ↗

SchemeTheory.SignPolynomial.polynomial_finiteType_quadratic

Documentation

The polynomial algebra has finite type over the quadratic subalgebra.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [Field k] (n : ℕ)

Lean source · statement

theorem polynomial_finiteType_quadratic :
    Algebra.FiniteType (quadraticSubalgebra k n) (MvPolynomial (Fin n) k)

theorem

quadratic_isInvariant

L40 ↗

SchemeTheory.SignPolynomial.quadratic_isInvariant

Documentation

Invariance uses the simultaneous sign action, rather than integer scalar multiplication.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [Field k] (n : ℕ)

Lean source · full declaration

theorem quadratic_isInvariant (htwo : (2 : k) ≠ 0) :
    let _action : MulSemiringAction ℤˣ (MvPolynomial (Fin n) k) := signAction k n
    Algebra.IsInvariant (quadraticSubalgebra k n) (MvPolynomial (Fin n) k) ℤˣ := by
  intro _action
  constructor
  intro p hp
  exact ⟨⟨p, (forall_signAction_iff_mem_quadraticSubalgebra k n htwo p).mp hp⟩, rfl⟩

theorem

polynomial_isIntegral_quadratic

L49 ↗

SchemeTheory.SignPolynomial.polynomial_isIntegral_quadratic

Documentation

Every polynomial is integral over the concrete quadratic subalgebra.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [Field k] (n : ℕ)

Lean source · statement

theorem polynomial_isIntegral_quadratic (htwo : (2 : k) ≠ 0) :
    Algebra.IsIntegral (quadraticSubalgebra k n) (MvPolynomial (Fin n) k)

theorem

polynomial_finite_quadratic

L59 ↗

SchemeTheory.SignPolynomial.polynomial_finite_quadratic

Documentation

The actual polynomial ring is a finite module over its quadratic subalgebra.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [Field k] (n : ℕ)

Lean source · statement

theorem polynomial_finite_quadratic (htwo : (2 : k) ≠ 0) :
    Module.Finite (quadraticSubalgebra k n) (MvPolynomial (Fin n) k)

Module documentation

Finiteness of the simultaneous sign quotient

Declarations

quadratic_finiteType

polynomial_finiteType_quadratic

quadratic_isInvariant

polynomial_isIntegral_quadratic

polynomial_finite_quadratic