Module

SmallHilbertPairingTransport.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.SmallHilbertPairingTransport

12 declarations indexed from sourceView source ↗

Module documentation

Transport of Hilbert pairings across field equivalences

The Type 0 local construction can be applied to a small representative of a local field. This file transports its public power-class and Kummer-norm statements back across the field equivalence.

Imports2

Imported by9

def

powerClassGroupEquivOfRingEquiv

L25 ↗

ClassFieldTheory.powerClassGroupEquivOfRingEquiv

Documentation

A field equivalence identifies the groups of n-th power classes.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

def powerClassGroupEquivOfRingEquiv
    {F : Type u} {G : Type v} [Field F] [Field G]
    (e : F ≃+* G) (n : ℕ+) :
    PowerClassGroup F n ≃* PowerClassGroup G n

def

rootsOfUnityEquivOfRingEquiv

L54 ↗

ClassFieldTheory.rootsOfUnityEquivOfRingEquiv

Documentation

A field equivalence identifies the n-th roots of unity.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

def rootsOfUnityEquivOfRingEquiv
    {F : Type u} {G : Type v} [Field F] [Field G]
    (e : F ≃+* G) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty) :
    rootsOfUnity (n : ℕ) F ≃* rootsOfUnity (n : ℕ) G

theorem

powerClassGroupEquivOfRingEquiv_powerClass

L63 ↗

ClassFieldTheory.powerClassGroupEquivOfRingEquiv_powerClass

Documentation

The image of a representative under the induced power-class equivalence.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

theorem powerClassGroupEquivOfRingEquiv_powerClass
    {F : Type u} {G : Type v} [Field F] [Field G]
    (e : F ≃+* G) (n : ℕ+) (a : Fˣ) :
    powerClassGroupEquivOfRingEquiv e n (powerClass F n a) =
      powerClass G n (Units.mapEquiv e.toMulEquiv a)

theorem

powerClassGroupEquivOfRingEquiv_symm_powerClass

L71 ↗

ClassFieldTheory.powerClassGroupEquivOfRingEquiv_symm_powerClass

Documentation

A representative pulled back from the target power-class group.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

theorem powerClassGroupEquivOfRingEquiv_symm_powerClass
    {F : Type u} {G : Type v} [Field F] [Field G]
    (e : F ≃+* G) (n : ℕ+) (a : Gˣ) :
    (powerClassGroupEquivOfRingEquiv e n).symm (powerClass G n a) =
      powerClass F n ((Units.mapEquiv e.toMulEquiv).symm a)

theorem

isKummerNorm_iff_of_ringEquiv

L82 ↗

ClassFieldTheory.isKummerNorm_iff_of_ringEquiv

Documentation

Kummer-algebra norm membership is invariant under a field equivalence, even when the Kummer polynomial is reducible.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

theorem isKummerNorm_iff_of_ringEquiv
    {F : Type u} {G : Type v} [Field F] [Field G]
    (e : F ≃+* G) (n : ℕ+) (a b : Fˣ) :
    IsKummerNorm F n a b ↔
      IsKummerNorm G n
        (Units.mapEquiv e.toMulEquiv a)
        (Units.mapEquiv e.toMulEquiv b)

def

hilbertPairingOfRingEquiv

L131 ↗

ClassFieldTheory.hilbertPairingOfRingEquiv

Documentation

Pull a pairing on power classes across an equivalence of base fields.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

def hilbertPairingOfRingEquiv
    {F : Type u} {G : Type v} [Field F] [Field G]
    (e : F ≃+* G) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (B : HilbertPairing F n) : HilbertPairing G n

theorem

hilbertPairingOfRingEquiv_apply

L147 ↗

ClassFieldTheory.hilbertPairingOfRingEquiv_apply

Documentation

Evaluation of a transported Hilbert pairing.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

theorem hilbertPairingOfRingEquiv_apply
    {F : Type u} {G : Type v} [Field F] [Field G]
    (e : F ≃+* G) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (B : HilbertPairing F n)
    (x y : PowerClassGroup G n) :
    hilbertPairingOfRingEquiv e n hmu B x y =
      rootsOfUnityEquivOfRingEquiv e n hmu
        (B ((powerClassGroupEquivOfRingEquiv e n).symm x)
          ((powerClassGroupEquivOfRingEquiv e n).symm y))

theorem

hilbertPairingOfRingEquiv_isSteinberg

L160 ↗

ClassFieldTheory.hilbertPairingOfRingEquiv_isSteinberg

Documentation

The Steinberg relation is preserved by base-field equivalence.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

theorem hilbertPairingOfRingEquiv_isSteinberg
    {F : Type u} {G : Type v} [Field F] [Field G]
    (e : F ≃+* G) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (B : HilbertPairing F n) (hB : B.IsSteinberg) :
    (hilbertPairingOfRingEquiv e n hmu B).IsSteinberg

theorem

hilbertPairingOfRingEquiv_isSkewSymmetric

L189 ↗

ClassFieldTheory.hilbertPairingOfRingEquiv_isSkewSymmetric

Documentation

Skew-symmetry is preserved by base-field equivalence.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

theorem hilbertPairingOfRingEquiv_isSkewSymmetric
    {F : Type u} {G : Type v} [Field F] [Field G]
    (e : F ≃+* G) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (B : HilbertPairing F n) (hB : B.IsSkewSymmetric) :
    (hilbertPairingOfRingEquiv e n hmu B).IsSkewSymmetric

theorem

hilbertPairingOfRingEquiv_isNondegenerate

L201 ↗

ClassFieldTheory.hilbertPairingOfRingEquiv_isNondegenerate

Documentation

Nondegeneracy in both variables is preserved by field equivalence.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

theorem hilbertPairingOfRingEquiv_isNondegenerate
    {F : Type u} {G : Type v} [Field F] [Field G]
    (e : F ≃+* G) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (B : HilbertPairing F n) (hB : B.IsNondegenerate) :
    (hilbertPairingOfRingEquiv e n hmu B).IsNondegenerate

theorem

hilbertPairingOfRingEquiv_satisfiesNormResidueCriterion

L236 ↗

ClassFieldTheory.hilbertPairingOfRingEquiv_satisfiesNormResidueCriterion

Documentation

The canonical Kummer norm-residue law is preserved by field equivalence.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

theorem hilbertPairingOfRingEquiv_satisfiesNormResidueCriterion
    {F : Type u} {G : Type v} [Field F] [Field G]
    (e : F ≃+* G) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (B : HilbertPairing F n) (hB : B.SatisfiesNormResidueCriterion) :
    (hilbertPairingOfRingEquiv e n hmu B).SatisfiesNormResidueCriterion

theorem

hilbertPairingOfRingEquiv_isLocalHilbertPairing

L270 ↗

ClassFieldTheory.hilbertPairingOfRingEquiv_isLocalHilbertPairing

Documentation

All public local-pairing properties are invariant under a field equivalence.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

theorem hilbertPairingOfRingEquiv_isLocalHilbertPairing
    {F : Type u} {G : Type v} [Field F] [Field G]
    (e : F ≃+* G) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (B : HilbertPairing F n)
    (hB : HilbertPairing.IsLocalHilbertPairing B) :
    HilbertPairing.IsLocalHilbertPairing
      (hilbertPairingOfRingEquiv e n hmu B)

Module documentation

Transport of Hilbert pairings across field equivalences

Declarations