The sign group as a line over `ZMod 2` #

Mathlib makes the two-element group ℤˣ = {±1}, written additively, a module over ZMod 2 (Mathlib.Data.ZMod.IntUnitsPower). This file records that it is the line ZMod 2: the map sending -1 to 1 is a ZMod 2-linear equivalence, so in particular the dimension is 1. This is what lets a family of ±1-valued characters indexed by a finite set ι be read as a linear map into a ZMod 2-space of dimension #ι, and lets such a family be compared with a family of ZMod 2-valued sign patterns.

Main results #

TauCeti.hilbertSign: the sign dictionary ZMod 2 → ℤˣ, sending 0 to 1 and 1 to -1.
TauCeti.additiveIntUnitsLinearEquiv: the linear equivalence Additive ℤˣ ≃ₗ[ZMod 2] ZMod 2.
TauCeti.finrank_zmod_two_additive_intUnits: Module.finrank (ZMod 2) (Additive ℤˣ) = 1.

source

def TauCeti.additiveIntUnitsAddEquiv :

Additive ℤ ˣ ≃+ ZMod 2

The sign group is the line ZMod 2. The additive form of ℤˣ = {±1} is isomorphic to ZMod 2, by the map sending 1 to 0 and -1 to 1. This is the unique isomorphism between the two groups, so no choice is involved.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem TauCeti.additiveIntUnitsAddEquiv_apply (u : Additive ℤ ˣ) :

additiveIntUnitsAddEquiv u = if Additive.toMul u = 1 then 0 else 1

source

def TauCeti.hilbertSign (x : ZMod 2) :

ℤ ˣ

Translate an additive ZMod 2 normalization, such as that of the cohomological local symbol, to the classical sign normalization, sending 0 to +1 and 1 to -1.

Equations

TauCeti.hilbertSign x = (AddEquiv.toMultiplicativeRight TauCeti.additiveIntUnitsAddEquiv).symm (Multiplicative.ofAdd x)

Instances For

source

@[simp]

theorem TauCeti.hilbertSign_zero :

hilbertSign 0 = 1

The zero class has positive sign.

source

@[simp]

theorem TauCeti.hilbertSign_one :

hilbertSign 1 = -1

The nonzero class in ZMod 2 has negative sign.

source

@[simp]

theorem TauCeti.hilbertSign_eq_one_iff (x : ZMod 2) :

hilbertSign x = 1 ↔ x = 0

The sign is +1 exactly at the zero class.

source

theorem TauCeti.hilbertSign_add (x y : ZMod 2) :

hilbertSign (x + y) = hilbertSign x * hilbertSign y

The sign dictionary turns addition of mod-two invariants into multiplication of signs.

source

def TauCeti.additiveIntUnitsLinearEquiv :

Additive ℤ ˣ ≃ₗ[ZMod 2] ZMod 2

The sign group is the line ZMod 2, linearly. TauCeti.additiveIntUnitsAddEquiv is automatically ZMod 2-linear, every additive map between ZMod 2-modules being so.

Equations