Module

SignPolynomialDegree.lean

Nyll.SchemeTheory.RingTheory.SignPolynomialDegree

10 declarations indexed from sourceView source ↗

Module documentation

Degree two of the actual simultaneous sign quotient

A nonempty set of variables makes the sign action faithful. The existing finite-group invariant-field theorem then gives ring rank two, and the canonical fraction-field extension has the same degree. No algebraic closure or characteristic-zero hypothesis is imposed.

Imports6

Nyll.SchemeTheory.RingTheory.SignPolynomialFinite
Mathlib.RingTheory.IsGaloisGroup.Defs
Mathlib.FieldTheory.Galois.IsGaloisGroup
Mathlib.LinearAlgebra.Dimension.Localization
Mathlib.Algebra.GroupWithZero.Units.Fintype
Mathlib.RingTheory.Localization.FractionRing

Imported by1

Nyll.SchemeTheory.RingTheory.All

def

fractionRingInclusion

L30 ↗

SchemeTheory.SignPolynomial.fractionRingInclusion

Documentation

The fraction-ring map induced by the original injective algebra map. The map, rather than a newly reconstructed scalar tower, owns the field extension.

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 fractionRingInclusion
    (A B : Type*) [CommRing A] [CommRing B] [IsDomain A] [IsDomain B]
    [Algebra A B] [FaithfulSMul A B] : FractionRing A →+* FractionRing B

theorem

fractionRingInclusion_algebraMap

L37 ↗

SchemeTheory.SignPolynomial.fractionRingInclusion_algebraMap

Documentation

The constructed fraction-ring map extends the original 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 fractionRingInclusion_algebraMap
    (A B : Type*) [CommRing A] [CommRing B] [IsDomain A] [IsDomain B]
    [Algebra A B] [FaithfulSMul A B] (a : A) :
    fractionRingInclusion A B (algebraMap A (FractionRing A) a) =
      algebraMap A (FractionRing B) a

theorem

fractionRingInclusion_isScalarTower

L46 ↗

SchemeTheory.SignPolynomial.fractionRingInclusion_isScalarTower

Source context 3 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial

Lean source · full declaration

theorem fractionRingInclusion_isScalarTower
    (A B : Type*) [CommRing A] [CommRing B] [IsDomain A] [IsDomain B]
    [Algebra A B] [FaithfulSMul A B] :
    let _fractionAlgebra : Algebra (FractionRing A) (FractionRing B) :=
      (fractionRingInclusion A B).toAlgebra
    IsScalarTower A (FractionRing A) (FractionRing B) := by
  intro _fractionAlgebra
  exact FractionRing.isScalarTower_liftAlgebra A (FractionRing B)

theorem

fractionRingInclusion_finrank

L57 ↗

SchemeTheory.SignPolynomial.fractionRingInclusion_finrank

Documentation

Rank compatibility for the actual fraction-ring inclusion, proved in a ring-only scope before the polynomial coefficient field is introduced.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial

Lean source · full declaration

theorem fractionRingInclusion_finrank
    (A B : Type*) [CommRing A] [CommRing B] [IsDomain A] [IsDomain B]
    [Algebra A B] [FaithfulSMul A B] :
    let _fractionAlgebra : Algebra (FractionRing A) (FractionRing B) :=
      (fractionRingInclusion A B).toAlgebra
    Module.finrank (FractionRing A) (FractionRing B) = Module.finrank A B := by
  intro _fractionAlgebra
  have hscalar : IsScalarTower A (FractionRing A) (FractionRing B) :=
    fractionRingInclusion_isScalarTower A B
  exact IsFractionRing.finrank_eq A (FractionRing A) B (FractionRing B)

theorem

simultaneousNeg_X_ne

L71 ↗

SchemeTheory.SignPolynomial.simultaneousNeg_X_ne

Documentation

A variable is moved by the sign involution in characteristic different from two.

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 simultaneousNeg_X_ne (htwo : (2 : k) ≠ 0) (i : Fin n) :
    simultaneousNeg k n (X i) ≠ (X i : MvPolynomial (Fin n) k)

theorem

signAction_faithful

L85 ↗

SchemeTheory.SignPolynomial.signAction_faithful

Documentation

The actual sign action is faithful as soon as one variable exists.

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 signAction_faithful (htwo : (2 : k) ≠ 0) (hn : 0 < n) :
    let _action : MulSemiringAction ℤˣ (MvPolynomial (Fin n) k) := signAction k n
    let _smul : SMul ℤˣ (MvPolynomial (Fin n) k) := _action.toSMul
    FaithfulSMul ℤˣ (MvPolynomial (Fin n) k) := by
  intro _action _smul
  constructor
  intro ε δ h
  let i : Fin n := ⟨0, hn⟩
  have hone : _action.smul (1 : ℤˣ) (X i) = X i := _action.one_smul (X i)
  have hneg : _action.smul (-1 : ℤˣ) (X i) = simultaneousNeg k n (X i) :=
    signAction_neg_one k n (X i)
  rcases Int.units_eq_one_or ε with rfl | rfl
  · rcases Int.units_eq_one_or δ with rfl | rfl
    · rfl
    · have hi : _action.smul (1 : ℤˣ) (X i) = _action.smul (-1 : ℤˣ) (X i) := h (X i)
      exact (simultaneousNeg_X_ne k n htwo i
        (hneg.symm.trans (hi.symm.trans hone))).elim
  · rcases Int.units_eq_one_or δ with rfl | rfl
    · have hi : _action.smul (-1 : ℤˣ) (X i) = _action.smul (1 : ℤˣ) (X i) := h (X i)
      exact (simultaneousNeg_X_ne k n htwo i
        (hneg.symm.trans (hi.trans hone))).elim
    · rfl

theorem

signAction_smulCommClass

L109 ↗

SchemeTheory.SignPolynomial.signAction_smulCommClass

Documentation

Multiplication by an invariant polynomial commutes with sign change.

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 signAction_smulCommClass (htwo : (2 : k) ≠ 0) :
    let _action : MulSemiringAction ℤˣ (MvPolynomial (Fin n) k) := signAction k n
    let _smul : SMul ℤˣ (MvPolynomial (Fin n) k) := _action.toSMul
    SMulCommClass ℤˣ (quadraticSubalgebra k n) (MvPolynomial (Fin n) k) := by
  intro _action _smul
  constructor
  intro ε a p
  rw [Algebra.smul_def, Algebra.smul_def, smul_mul']
  have ha : _action.smul ε (a : MvPolynomial (Fin n) k) = a :=
    (forall_signAction_iff_mem_quadraticSubalgebra k n htwo a).mpr a.property ε
  rw [Subalgebra.algebraMap_apply]
  exact congrArg (fun q : MvPolynomial (Fin n) k => q * _action.smul ε p) ha

theorem

quadratic_isGaloisGroup

L123 ↗

SchemeTheory.SignPolynomial.quadratic_isGaloisGroup

Documentation

The order-two group is the Galois group of the literal ring extension B/A.

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_isGaloisGroup (htwo : (2 : k) ≠ 0) (hn : 0 < n) :
    let _action : MulSemiringAction ℤˣ (MvPolynomial (Fin n) k) := signAction k n
    IsGaloisGroup ℤˣ (quadraticSubalgebra k n) (MvPolynomial (Fin n) k) := by
  intro _action
  let _smul : SMul ℤˣ (MvPolynomial (Fin n) k) := _action.toSMul
  exact ⟨signAction_faithful k n htwo hn, signAction_smulCommClass k n htwo,
    quadratic_isInvariant k n htwo⟩

theorem

polynomial_finrank_quadratic

L132 ↗

SchemeTheory.SignPolynomial.polynomial_finrank_quadratic

Documentation

The polynomial ring has rank two over the quadratic invariant 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_finrank_quadratic (htwo : (2 : k) ≠ 0) (hn : 0 < n) :
    Module.finrank (quadraticSubalgebra k n) (MvPolynomial (Fin n) k) = 2

theorem

fractionRing_finrank_quadratic

L142 ↗

SchemeTheory.SignPolynomial.fractionRing_finrank_quadratic

Documentation

The actual fraction-field extension, induced from the original inclusion, has degree two.

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 fractionRing_finrank_quadratic (htwo : (2 : k) ≠ 0) (hn : 0 < n) :
    let _fractionAlgebra : Algebra (FractionRing (quadraticSubalgebra k n))
        (FractionRing (MvPolynomial (Fin n) k)) :=
      (fractionRingInclusion (quadraticSubalgebra k n)
        (MvPolynomial (Fin n) k)).toAlgebra
    Module.finrank (FractionRing (quadraticSubalgebra k n))
      (FractionRing (MvPolynomial (Fin n) k)) = 2 := by
  intro _fractionAlgebra
  rw [fractionRingInclusion_finrank (quadraticSubalgebra k n) (MvPolynomial (Fin n) k)]
  exact polynomial_finrank_quadratic k n htwo hn

Module documentation

Degree two of the actual simultaneous sign quotient

Declarations