Module

PrimePowerKernelCoordinates.lean

Nyll.GaloisCohomology.Kummer.Concrete.SUnitPreparation.PrimePowerKernelCoordinates

9 declarations indexed from sourceView source ↗

Module documentation

Prime-power kernel coordinates

Linear-algebraic coordinates for kernels of surjections between finite free modules over ZMod (p ^ v).

Imports6

Mathlib.Algebra.Group.Equiv.TypeTags
Mathlib.Algebra.Module.ZMod
Mathlib.Data.Finsupp.Fintype
Mathlib.Data.ZMod.Basic
Mathlib.FieldTheory.IntermediateField.Basic
Mathlib.RingTheory.LocalRing.Module

Imported by8

theorem

zmodPrimePower_isLocalRing

L32 ↗

KummerTheory.zmodPrimePower_isLocalRing

Documentation

A prime-power residue ring is local. This instance is the algebraic input needed to turn the projective kernel in the finite S-unit preparation argument into a free ZMod (p ^ v)-module.

Source context 3 commands

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

open scoped IsMulCommutative
noncomputable section
namespace KummerTheory

Lean source · statement

theorem zmodPrimePower_isLocalRing
    (p v : ℕ) (hp : p.Prime) (hv : 0 < v) :
    IsLocalRing (ZMod (p ^ v))

theorem

free_ker_of_surjective_linearMap_of_isLocalRing

L82 ↗

KummerTheory.free_ker_of_surjective_linearMap_of_isLocalRing

Documentation

Over a local ring, the kernel of a surjection between finite free modules is free. The proof constructs the splitting explicitly and then uses finite projective modules over local rings.

Source context 3 commands

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

open scoped IsMulCommutative
noncomputable section
namespace KummerTheory

Lean source · statement

theorem free_ker_of_surjective_linearMap_of_isLocalRing
    {R M N : Type*} [CommRing R] [IsLocalRing R]
    [AddCommGroup M] [AddCommGroup N]
    [Module R M] [Module R N]
    [Module.Free R M] [Module.Free R N]
    [Finite M]
    (f : M →ₗ[R] N) (hf : Function.Surjective f) :
    Module.Free R (LinearMap.ker f)

theorem

card_eq_card_pow_card_chooseBasisIndex

L123 ↗

KummerTheory.card_eq_card_pow_card_chooseBasisIndex

Documentation

The cardinality of a finite free module is the cardinality of the coefficient ring raised to the size of a chosen basis.

Source context 3 commands

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

open scoped IsMulCommutative
noncomputable section
namespace KummerTheory

Lean source · statement

theorem card_eq_card_pow_card_chooseBasisIndex
    {R M : Type*} [Semiring R]
    [AddCommMonoid M] [Module R M]
    [Module.Free R M] [Finite R] [Finite M] :
    Nat.card M =
      Nat.card R ^
        Fintype.card (Module.Free.ChooseBasisIndex R M)

def

additiveCoordinatesLinearEquiv

L143 ↗

KummerTheory.additiveCoordinatesLinearEquiv

Documentation

Multiplicative product coordinates, interpreted as a ZMod n-linear equivalence on the additive presentations.

Source context 3 commands

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

open scoped IsMulCommutative
noncomputable section
namespace KummerTheory

Lean source · statement

def additiveCoordinatesLinearEquiv
    {G A B : Type*} [CommGroup G] [AddCommGroup A]
    [AddCommGroup B] (n : ℕ)
    [Module (ZMod n) (Additive G)]
    [Module (ZMod n) A] [Module (ZMod n) B]
    (e : G ≃* Multiplicative A × Multiplicative B) :
    Additive G ≃ₗ[ZMod n] A × B

def

additiveZModModuleOfPowEqOne

L160 ↗

KummerTheory.additiveZModModuleOfPowEqOne

Documentation

The canonical ZMod n-module on the additive presentation of a commutative group of exponent dividing n.

Source context 3 commands

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

open scoped IsMulCommutative
noncomputable section
namespace KummerTheory

Lean source · statement

def additiveZModModuleOfPowEqOne
    {G : Type*} [CommGroup G] (n : ℕ)
    (h : ∀ g : G, g ^ n = 1) :
    Module (ZMod n) (Additive G)

def

additivePiLinearEquiv

L171 ↗

KummerTheory.additivePiLinearEquiv

Documentation

Multiplicative function coordinates, interpreted as a ZMod n-linear equivalence on the additive presentations.

Source context 3 commands

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

open scoped IsMulCommutative
noncomputable section
namespace KummerTheory

Lean source · statement

def additivePiLinearEquiv
    {G A : Type*} [CommGroup G] [AddCommGroup A]
    {ι : Type*} (n : ℕ)
    [Module (ZMod n) (Additive G)]
    [Module (ZMod n) A]
    (e : G ≃* (ι → Multiplicative A)) :
    Additive G ≃ₗ[ZMod n] (ι → A)

def

monoidKerEquivMultiplicativeLinearKer

L187 ↗

KummerTheory.monoidKerEquivMultiplicativeLinearKer

Documentation

The multiplicative kernel of a homomorphism is the multiplicative presentation of the kernel of its induced ZMod n-linear map.

Source context 3 commands

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

open scoped IsMulCommutative
noncomputable section
namespace KummerTheory

Lean source · full declaration

def monoidKerEquivMultiplicativeLinearKer
    {G H : Type*} [CommGroup G] [CommGroup H]
    (n : ℕ)
    [Module (ZMod n) (Additive G)]
    [Module (ZMod n) (Additive H)]
    (f : G →* H) :
    f.ker ≃*
      Multiplicative
        (LinearMap.ker
          (f.toAdditive.toZModLinearMap n)) where
  toFun x :=
    Multiplicative.ofAdd
      ⟨Additive.ofMul x.1, by
        rw [LinearMap.mem_ker]
        apply Additive.toMul.injective
        exact x.2⟩
  invFun x :=
    ⟨Additive.toMul (Multiplicative.toAdd x).1, by
      change f (Additive.toMul (Multiplicative.toAdd x).1) = 1
      have hx := (Multiplicative.toAdd x).2
      rw [LinearMap.mem_ker] at hx
      exact congrArg Additive.toMul hx⟩
  left_inv x := by
    apply Subtype.ext
    rfl
  right_inv x := by
    apply Multiplicative.toAdd.injective
    apply Subtype.ext
    rfl
  map_mul' x y := by
    apply Multiplicative.toAdd.injective
    apply Subtype.ext
    rfl

theorem

exists_kernelMulEquiv_pi_zmod_of_primePower

L224 ↗

KummerTheory.exists_kernelMulEquiv_pi_zmod_of_primePower

Documentation

A surjection between finite free ZMod (p ^ v)-modules has a kernel with genuine coordinates. Its number of coordinates is read off from the cardinality of the kernel.

Source context 3 commands

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

open scoped IsMulCommutative
noncomputable section
namespace KummerTheory

Lean source · statement

theorem exists_kernelMulEquiv_pi_zmod_of_primePower
    {G H : Type*} [CommGroup G] [CommGroup H]
    (n p v q : ℕ)
    (hp : p.Prime) (hv : 0 < v)
    (hn : n = p ^ v)
    [Module (ZMod n) (Additive G)]
    [Module (ZMod n) (Additive H)]
    (freeG : Module.Free (ZMod n) (Additive G))
    (freeH : Module.Free (ZMod n) (Additive H))
    [Finite G]
    (f : G →* H) (hf : Function.Surjective f)
    (hcard : Nat.card f.ker = n ^ q) :
    Nonempty
      (f.ker ≃*
        (Fin q → Multiplicative (ZMod n)))

theorem

galois_pow_eq_one_of_equiv_pi_zmod

L310 ↗

KummerTheory.galois_pow_eq_one_of_equiv_pi_zmod

Documentation

The exponent-n statement read directly from coordinates Gal(E/K) ≃ (Z/nZ)^r.

Source context 3 commands

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

open scoped IsMulCommutative
noncomputable section
namespace KummerTheory

Lean source · statement

theorem galois_pow_eq_one_of_equiv_pi_zmod
    {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
    (E : IntermediateField K Omega)
    (n : ℕ+) (r : ℕ)
    (eG :
      (E ≃ₐ[K] E) ≃*
        (Fin r → Multiplicative (ZMod (n : ℕ))))
    (sigma : E ≃ₐ[K] E) :
    sigma ^ (n : ℕ) = 1

Module documentation

Prime-power kernel coordinates

Declarations