Module

SignPolynomialNormal.lean

Nyll.SchemeTheory.RingTheory.SignPolynomialNormal

9 declarations indexed from sourceView source ↗

Module documentation

Normality and the integral closure for the sign quotient

Normality descends because a polynomial quotient of two invariant polynomials is itself invariant. The polynomial ring is the integral closure of the quadratic subalgebra in its own fraction field, using its original inclusion.

Imports7

Nyll.SchemeTheory.RingTheory.SignPolynomialFinite
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Mathlib.RingTheory.Polynomial.UniqueFactorization
Mathlib.RingTheory.Polynomial.RationalRoot
Mathlib.RingTheory.Localization.FractionRing
Mathlib.Algebra.Algebra.Subalgebra.Tower

Imported by1

Nyll.SchemeTheory.RingTheory.All

def

subringFractionLift

L29 ↗

SchemeTheory.SignPolynomial.subringFractionLift

Documentation

The canonical inclusion of fraction rings, using only ring-hom data.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial

Lean source · statement

def subringFractionLift
    {B : Type*} [CommRing B] [IsDomain B] (S : Subring B) :
    FractionRing S →+* FractionRing B

theorem

subringFractionLift_algebraMap

L36 ↗

SchemeTheory.SignPolynomial.subringFractionLift_algebraMap

Documentation

The fraction inclusion extends the original subtype inclusion.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial

Lean source · statement

theorem subringFractionLift_algebraMap
    {B : Type*} [CommRing B] [IsDomain B] (S : Subring B) (a : S) :
    subringFractionLift S (algebraMap S (FractionRing S) a) =
      algebraMap B (FractionRing B) (a : B)

theorem

subringFractionLift_isIntegral

L45 ↗

SchemeTheory.SignPolynomial.subringFractionLift_isIntegral

Documentation

Transport integrality through the literal commuting square of ring maps.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial

Lean source · statement

theorem subringFractionLift_isIntegral
    {B : Type*} [CommRing B] [IsDomain B] (S : Subring B)
    (x : FractionRing S) (hx : IsIntegral S x) :
    IsIntegral B (subringFractionLift S x)

theorem

fractionRing_exists_div_ne_zero

L55 ↗

SchemeTheory.SignPolynomial.fractionRing_exists_div_ne_zero

Documentation

Choose a fraction presentation with its denominator nonzero in the base ring.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial

Lean source · statement

theorem fractionRing_exists_div_ne_zero
    (R : Type*) [CommRing R] [IsDomain R] (x : FractionRing R) :
    ∃ a d : R, d ≠ 0 ∧
      algebraMap R (FractionRing R) a / algebraMap R (FractionRing R) d = x

theorem

subringFractionLift_preimage

L64 ↗

SchemeTheory.SignPolynomial.subringFractionLift_preimage

Documentation

A fraction whose image is a polynomial already comes from the subring when that subring is closed under quotients in the ambient ring.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial

Lean source · statement

theorem subringFractionLift_preimage
    {B : Type*} [CommRing B] [IsDomain B] (S : Subring B)
    (hdiv : ∀ (b : B) (a : S), a ≠ 0 → b * (a : B) ∈ S → b ∈ S)
    (x : FractionRing S) (b : B)
    (hb : algebraMap B (FractionRing B) b = subringFractionLift S x) :
    ∃ a : S, algebraMap S (FractionRing S) a = x

theorem

subring_isIntegrallyClosed_of_mul_mem

L92 ↗

SchemeTheory.SignPolynomial.subring_isIntegrallyClosed_of_mul_mem

Source context 3 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial

Lean source · statement

theorem subring_isIntegrallyClosed_of_mul_mem
    {B : Type*} [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
    (S : Subring B)
    (hdiv : ∀ (b : B) (a : S), a ≠ 0 → b * (a : B) ∈ S → b ∈ S) :
    IsIntegrallyClosed S

theorem

mem_quadratic_of_mul_mem

L106 ↗

SchemeTheory.SignPolynomial.mem_quadratic_of_mul_mem

Documentation

A polynomial quotient with invariant nonzero denominator is invariant.

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 mem_quadratic_of_mul_mem (htwo : (2 : k) ≠ 0)
    (p : MvPolynomial (Fin n) k) (a : quadraticSubalgebra k n)
    (ha : a ≠ 0) (hpa : p * (a : MvPolynomial (Fin n) k) ∈ quadraticSubalgebra k n) :
    p ∈ quadraticSubalgebra k n

theorem

quadratic_isIntegrallyClosed

L128 ↗

SchemeTheory.SignPolynomial.quadratic_isIntegrallyClosed

Documentation

The quadratic invariant subalgebra is a normal domain.

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_isIntegrallyClosed (htwo : (2 : k) ≠ 0) :
    IsIntegrallyClosed (quadraticSubalgebra k n)

theorem

polynomial_isIntegralClosure_quadratic

L134 ↗

SchemeTheory.SignPolynomial.polynomial_isIntegralClosure_quadratic

Documentation

The original polynomial ring is the integral closure in its fraction 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 polynomial_isIntegralClosure_quadratic (htwo : (2 : k) ≠ 0) :
    IsIntegralClosure (MvPolynomial (Fin n) k) (quadraticSubalgebra k n)
      (FractionRing (MvPolynomial (Fin n) k))

Module documentation

Normality and the integral closure for the sign quotient

Declarations