NYLL
Module

SignPolynomialAction.lean

Nyll.SchemeTheory.RingTheory.SignPolynomialAction
15 declarations indexed from sourceView source ↗

Module documentation

Simultaneous sign change on the polynomial ring

The sign group is the concrete group ℤˣ = {1, -1}. Its action is kept as explicit data, so no competing action on the polynomial ring is registered. This is the action occurring in Stacks Project, Tag 0BTE.

Imports7
  • Mathlib.Algebra.MvPolynomial.Basic
  • Mathlib.Algebra.MvPolynomial.Eval
  • Mathlib.Algebra.MvPolynomial.CommRing
  • Mathlib.Algebra.Algebra.Equiv
  • Mathlib.Algebra.Algebra.Subalgebra.Basic
  • Mathlib.Algebra.Ring.Action.Basic
  • Mathlib.Algebra.Ring.Int.Units
Imported by2

Declarations

def

simultaneousNegHom

L31 ↗
SchemeTheory.SignPolynomial.simultaneousNegHom
Documentation

Simultaneous negation of all polynomial variables as an algebra homomorphism.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [CommRing k] (n : ℕ)
Lean source · statement
def simultaneousNegHom : MvPolynomial (Fin n) k →ₐ[k] MvPolynomial (Fin n) k
theorem

simultaneousNegHom_comp_self

L34 ↗
SchemeTheory.SignPolynomial.simultaneousNegHom_comp_self
Source context 4 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [CommRing k] (n : ℕ)
Lean source · statement
theorem simultaneousNegHom_comp_self :
    (simultaneousNegHom k n).comp (simultaneousNegHom k n) =
      AlgHom.id k (MvPolynomial (Fin n) k)
def

simultaneousNeg

L43 ↗
SchemeTheory.SignPolynomial.simultaneousNeg
Documentation

The actual algebra involution sending every X i to -X i.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [CommRing k] (n : ℕ)
Lean source · statement
def simultaneousNeg : MvPolynomial (Fin n) k ≃ₐ[k] MvPolynomial (Fin n) k
theorem

simultaneousNeg_apply

L47 ↗
SchemeTheory.SignPolynomial.simultaneousNeg_apply
Source context 4 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [CommRing k] (n : ℕ)
Lean source · statement
theorem simultaneousNeg_apply (p : MvPolynomial (Fin n) k) :
    simultaneousNeg k n p = simultaneousNegHom k n p
theorem

simultaneousNeg_X

L51 ↗
SchemeTheory.SignPolynomial.simultaneousNeg_X
Source context 4 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [CommRing k] (n : ℕ)
Lean source · statement
theorem simultaneousNeg_X (i : Fin n) :
    simultaneousNeg k n (X i) = -X i
theorem

simultaneousNeg_involutive

L55 ↗
SchemeTheory.SignPolynomial.simultaneousNeg_involutive
Source context 4 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [CommRing k] (n : ℕ)
Lean source · statement
theorem simultaneousNeg_involutive : Function.Involutive (simultaneousNeg k n)
theorem

simultaneousNeg_mul_self

L59 ↗
SchemeTheory.SignPolynomial.simultaneousNeg_mul_self
Source context 4 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [CommRing k] (n : ℕ)
Lean source · statement
theorem simultaneousNeg_mul_self : simultaneousNeg k n * simultaneousNeg k n = 1
def

signActionHom

L65 ↗
SchemeTheory.SignPolynomial.signActionHom
Documentation

The action homomorphism of the two-element group of integer units.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [CommRing k] (n : ℕ)
Lean source · full declaration
def signActionHom : ℤˣ →* (MvPolynomial (Fin n) k ≃ₐ[k] MvPolynomial (Fin n) k) where
  toFun ε := if ε = 1 then 1 else simultaneousNeg k n
  map_one' := ite_eq_left rfl
  map_mul' ε δ := by
    rcases Int.units_eq_one_or ε with rfl | rfl
    · simp only [one_mul, ite_true]
    · rcases Int.units_eq_one_or δ with rfl | rfl
      · simp only [mul_one, ite_true]
      · have hneg : (-1 : ℤˣ) ≠ 1 := by decide
        have hmul : (-1 : ℤˣ) * (-1) = 1 := by decide
        simp only [hmul, ite_true, ite_eq_right hneg, simultaneousNeg_mul_self]
theorem

signActionHom_apply

L77 ↗
SchemeTheory.SignPolynomial.signActionHom_apply
Source context 4 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [CommRing k] (n : ℕ)
Lean source · full declaration
theorem signActionHom_apply (ε : ℤˣ) :
    signActionHom k n ε = if ε = 1 then 1 else simultaneousNeg k n := rfl
def

signAction

L82 ↗
SchemeTheory.SignPolynomial.signAction
Documentation

The sign action on the polynomial algebra, supplied as explicit data.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [CommRing k] (n : ℕ)
Lean source · statement
def signAction : MulSemiringAction ℤˣ (MvPolynomial (Fin n) k)
theorem

signAction_neg_one

L85 ↗
SchemeTheory.SignPolynomial.signAction_neg_one
Source context 4 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [CommRing k] (n : ℕ)
Lean source · statement
theorem signAction_neg_one (p : MvPolynomial (Fin n) k) :
    (signAction k n).smul (-1 : ℤˣ) p = simultaneousNeg k n p
theorem

signAction_fixed_iff

L92 ↗
SchemeTheory.SignPolynomial.signAction_fixed_iff
Documentation

Fixed by the entire sign group is equivalent to fixed by simultaneous negation.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [CommRing k] (n : ℕ)
Lean source · statement
theorem signAction_fixed_iff (p : MvPolynomial (Fin n) k) :
    (∀ ε : ℤˣ, (signAction k n).smul ε p = p) ↔ simultaneousNeg k n p = p
def

fixedSubalgebra

L105 ↗
SchemeTheory.SignPolynomial.fixedSubalgebra
Documentation

The fixed subalgebra of the simultaneous sign action.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [CommRing k] (n : ℕ)
Lean source · statement
def fixedSubalgebra : Subalgebra k (MvPolynomial (Fin n) k)
theorem

mem_fixedSubalgebra_iff

L108 ↗
SchemeTheory.SignPolynomial.mem_fixedSubalgebra_iff
Source context 4 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [CommRing k] (n : ℕ)
Lean source · statement
theorem mem_fixedSubalgebra_iff (p : MvPolynomial (Fin n) k) :
    p ∈ fixedSubalgebra k n ↔ simultaneousNeg k n p = p
theorem

mem_fixedSubalgebra_iff_forall_signAction

L111 ↗
SchemeTheory.SignPolynomial.mem_fixedSubalgebra_iff_forall_signAction
Source context 4 commands

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

noncomputable section
namespace SchemeTheory.SignPolynomial
open MvPolynomial
variable (k : Type*) [CommRing k] (n : ℕ)
Lean source · statement
theorem mem_fixedSubalgebra_iff_forall_signAction (p : MvPolynomial (Fin n) k) :
    p ∈ fixedSubalgebra k n ↔ ∀ ε : ℤˣ, (signAction k n).smul ε p = p

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.