Module

FiniteDualSeparation.lean

Nyll.GaloisCohomology.Kummer.Concrete.FiniteDualSeparation

16 declarations indexed from sourceView source ↗

Module documentation

finite Kummer dual separation

This file supplies the first missing finite-duality source for the full subgroup/extension correspondence in the Kummer correspondence. Characters of a finite abelian group killed by n can be chosen with values in μₙ, and these characters separate points. Consequently, the transpose of a character equivalence R ≃ Hom(G, μₙ) is injective.

No lattice correspondence or infinite Kummer endpoint is asserted here.

Imports1

Nyll.GaloisCohomology.Kummer.Concrete.FiniteGeneration

Imported by10

def

characterToNthRoots

L29 ↗

KummerTheory.characterToNthRoots

Documentation

Restrict a unit-valued character to μₙ when its source is killed by n.

Source context 2 commands

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

noncomputable section
namespace KummerTheory

Lean source · full declaration

def characterToNthRoots
    {G K : Type*} [Group G] [Field K]
    (n : ℕ+) (hexponent : ∀ g : G, g ^ (n : ℕ) = 1)
    (φ : G →* Kˣ) : G →* nthRootsSubgroup K (n : ℕ) where
  toFun g :=
    ⟨φ g, by
      calc
        φ g ^ (n : ℕ) = φ (g ^ (n : ℕ)) := (map_pow φ g (n : ℕ)).symm
        _ = 1 := by rw [hexponent g, map_one]⟩
  map_one' := by
    apply Subtype.ext
    exact map_one φ
  map_mul' := by
    intro g h
    apply Subtype.ext
    exact map_mul φ g h

theorem

characterToNthRoots_apply

L47 ↗

KummerTheory.characterToNthRoots_apply

Documentation

A finite character evaluates in the subgroup of nth roots of unity.

Source context 2 commands

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

noncomputable section
namespace KummerTheory

Lean source · statement

theorem characterToNthRoots_apply
    {G K : Type*} [Group G] [Field K]
    (n : ℕ+) (hexponent : ∀ g : G, g ^ (n : ℕ) = 1)
    (φ : G →* Kˣ) (g : G) :
    (characterToNthRoots n hexponent φ g : Kˣ) = φ g

theorem

exists_nthRoots_character_apply_ne_one

L56 ↗

KummerTheory.exists_nthRoots_character_apply_ne_one

Documentation

Characters with values in the actual n-th roots of unity of K separate points of a finite abelian group killed by n.

Source context 2 commands

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

noncomputable section
namespace KummerTheory

Lean source · statement

theorem exists_nthRoots_character_apply_ne_one
    {G K : Type*} [CommGroup G] [Finite G] [Field K]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ g : G, g ^ (n : ℕ) = 1)
    {g : G} (hg : g ≠ 1) :
    ∃ χ : G →* nthRootsSubgroup K (n : ℕ), χ g ≠ 1

def

nthRootsSubgroupMap

L82 ↗

KummerTheory.nthRootsSubgroupMap

Documentation

Algebraic extension maps carry μₙ(K) injectively into μₙ(L).

Source context 2 commands

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

noncomputable section
namespace KummerTheory

Lean source · full declaration

def nthRootsSubgroupMap
    (K L : Type*) [Field K] [Field L] [Algebra K L] (n : ℕ) :
    nthRootsSubgroup K n →* nthRootsSubgroup L n where
  toFun z :=
    ⟨Units.map (algebraMap K L).toMonoidHom z.1, by
      calc
        Units.map (algebraMap K L).toMonoidHom z.1 ^ n =
            Units.map (algebraMap K L).toMonoidHom (z.1 ^ n) :=
          (map_pow (Units.map (algebraMap K L).toMonoidHom) z.1 n).symm
        _ = 1 := by rw [z.2, map_one]⟩
  map_one' := by
    apply Subtype.ext
    exact map_one (Units.map (algebraMap K L).toMonoidHom)
  map_mul' := by
    intro z w
    apply Subtype.ext
    exact map_mul (Units.map (algebraMap K L).toMonoidHom) z.1 w.1

theorem

nthRootsSubgroupMap_injective

L101 ↗

KummerTheory.nthRootsSubgroupMap_injective

Documentation

The canonical map from roots of unity into the nth-roots subgroup is injective.

Source context 2 commands

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

noncomputable section
namespace KummerTheory

Lean source · statement

theorem nthRootsSubgroupMap_injective
    (K L : Type*) [Field K] [Field L] [Algebra K L] (n : ℕ) :
    Function.Injective (nthRootsSubgroupMap K L n)

def

nthRootsSubgroupEquivRootsOfUnity

L112 ↗

KummerTheory.nthRootsSubgroupEquivRootsOfUnity

Documentation

The locally defined nthRootsSubgroup is canonically the same group as mathlib's rootsOfUnity.

Source context 2 commands

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

noncomputable section
namespace KummerTheory

Lean source · full declaration

def nthRootsSubgroupEquivRootsOfUnity
    (K : Type*) [Field K] (n : ℕ) :
    nthRootsSubgroup K n ≃* rootsOfUnity n K where
  toFun z := ⟨z.1, z.2⟩
  invFun z := ⟨z.1, z.2⟩
  left_inv _ := rfl
  right_inv _ := rfl
  map_mul' _ _ := rfl

instance

nthRootsSubgroupFintype

L122 ↗

KummerTheory.nthRootsSubgroupFintype

Documentation

The subgroup of nth roots of unity has a canonical finite type structure.

Source context 2 commands

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

noncomputable section
namespace KummerTheory

Lean source · statement

instance nthRootsSubgroupFintype
    (K : Type*) [Field K] (n : ℕ) [NeZero n] : Fintype (nthRootsSubgroup K n)

def

nthRootsSubgroupEquivOfPrimitiveRoots

L130 ↗

KummerTheory.nthRootsSubgroupEquivOfPrimitiveRoots

Documentation

If K contains a primitive n-th root, extension of scalars identifies the n-th roots of unity in K and in every extension field L.

Source context 2 commands

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

noncomputable section
namespace KummerTheory

Lean source · statement

def nthRootsSubgroupEquivOfPrimitiveRoots
    (K L : Type*) [Field K] [Field L] [Algebra K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    nthRootsSubgroup K (n : ℕ) ≃* nthRootsSubgroup L (n : ℕ)

def

unitCharactersEquivNthRoots

L155 ↗

KummerTheory.unitCharactersEquivNthRoots

Documentation

For a group killed by n, restricting a Kˣ-valued character to μₙ(K) loses no information.

Source context 2 commands

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

noncomputable section
namespace KummerTheory

Lean source · full declaration

def unitCharactersEquivNthRoots
    {G K : Type*} [CommGroup G] [Field K]
    (n : ℕ+) (hexponent : ∀ g : G, g ^ (n : ℕ) = 1) :
    (G →* Kˣ) ≃* (G →* nthRootsSubgroup K (n : ℕ)) where
  toFun := characterToNthRoots n hexponent
  invFun χ := (nthRootsSubgroup K (n : ℕ)).subtype.comp χ
  left_inv φ := by
    apply MonoidHom.ext
    intro g
    rfl
  right_inv χ := by
    apply MonoidHom.ext
    intro g
    apply Subtype.ext
    rfl
  map_mul' φ ψ := by
    apply MonoidHom.ext
    intro g
    apply Subtype.ext
    rfl

theorem

finiteNthRootsCharacterDuality

L178 ↗

KummerTheory.finiteNthRootsCharacterDuality

Documentation

Finite abelian duality with the character codomain restricted to the actual n-th roots of unity in an extension field.

Source context 2 commands

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

noncomputable section
namespace KummerTheory

Lean source · statement

theorem finiteNthRootsCharacterDuality
    {G K L : Type*} [CommGroup G] [Finite G]
    [Field K] [Field L] [Algebra K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ g : G, g ^ (n : ℕ) = 1) :
    Nonempty ((G →* nthRootsSubgroup L (n : ℕ)) ≃* G)

theorem

exists_nthRoots_character_apply_ne_one_in_extension

L203 ↗

KummerTheory.exists_nthRoots_character_apply_ne_one_in_extension

Documentation

The same separation result with values in the roots of unity of an extension field L.

Source context 2 commands

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

noncomputable section
namespace KummerTheory

Lean source · statement

theorem exists_nthRoots_character_apply_ne_one_in_extension
    {G K L : Type*} [CommGroup G] [Finite G]
    [Field K] [Field L] [Algebra K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ g : G, g ^ (n : ℕ) = 1)
    {g : G} (hg : g ≠ 1) :
    ∃ χ : G →* nthRootsSubgroup L (n : ℕ), χ g ≠ 1

def

transposeCharacterEquiv

L219 ↗

KummerTheory.transposeCharacterEquiv

Documentation

Transpose a character equivalence by evaluation.

Source context 2 commands

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

noncomputable section
namespace KummerTheory

Lean source · full declaration

def transposeCharacterEquiv
    {G R M : Type*} [CommGroup G] [CommGroup R] [CommGroup M]
    (e : R ≃* (G →* M)) : G →* (R →* M) where
  toFun g :=
    { toFun := fun r => e r g
      map_one' := by simp
      map_mul' := by
        intro r s
        exact congrArg (fun χ : G →* M => χ g) (map_mul e r s) }
  map_one' := by
    apply MonoidHom.ext
    intro r
    exact map_one (e r)
  map_mul' := by
    intro g h
    apply MonoidHom.ext
    intro r
    exact map_mul (e r) g h

theorem

transposeCharacterEquiv_apply

L239 ↗

KummerTheory.transposeCharacterEquiv_apply

Documentation

The transposed character equivalence evaluates by pairing with the original character.

Source context 2 commands

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

noncomputable section
namespace KummerTheory

Lean source · statement

theorem transposeCharacterEquiv_apply
    {G R M : Type*} [CommGroup G] [CommGroup R] [CommGroup M]
    (e : R ≃* (G →* M)) (g : G) (r : R) :
    transposeCharacterEquiv e g r = e r g

theorem

transposeCharacterEquiv_injective

L248 ↗

KummerTheory.transposeCharacterEquiv_injective

Documentation

Nondegeneracy on the Galois side of the finite Kummer pairing. This is the injectivity source needed before the cardinality step can upgrade the transpose to the canonical isomorphism in the Kummer correspondence.

Source context 2 commands

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

noncomputable section
namespace KummerTheory

Lean source · statement

theorem transposeCharacterEquiv_injective
    {G R K L : Type*} [CommGroup G] [Finite G] [CommGroup R]
    [Field K] [Field L] [Algebra K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ g : G, g ^ (n : ℕ) = 1)
    (e : R ≃* (G →* nthRootsSubgroup L (n : ℕ))) :
    Function.Injective (transposeCharacterEquiv e)

theorem

transposeCharacterEquiv_surjective

L274 ↗

KummerTheory.transposeCharacterEquiv_surjective

Documentation

The finite cardinality step upgrades nondegeneracy of the transposed Kummer pairing to surjectivity. The needed equality of cardinalities is produced by finite abelian duality; it is not assumed.

Source context 2 commands

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

noncomputable section
namespace KummerTheory

Lean source · statement

theorem transposeCharacterEquiv_surjective
    {G R K L : Type*} [CommGroup G] [Finite G] [CommGroup R]
    [Field K] [Field L] [Algebra K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ g : G, g ^ (n : ℕ) = 1)
    (e : R ≃* (G →* nthRootsSubgroup L (n : ℕ))) :
    Function.Surjective (transposeCharacterEquiv e)

def

transposeCharacterMulEquiv

L308 ↗

KummerTheory.transposeCharacterMulEquiv

Documentation

The canonical finite Kummer transpose equivalence. This is the finite perfect-pairing equivalence underlying the Galois-group isomorphism; it does not yet assert the subgroup/extension lattice endpoint.

Source context 2 commands

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

noncomputable section
namespace KummerTheory

Lean source · statement

def transposeCharacterMulEquiv
    {G R K L : Type*} [CommGroup G] [Finite G] [CommGroup R]
    [Field K] [Field L] [Algebra K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ g : G, g ^ (n : ℕ) = 1)
    (e : R ≃* (G →* nthRootsSubgroup L (n : ℕ))) :
    G ≃* (R →* nthRootsSubgroup L (n : ℕ))

Module documentation

finite Kummer dual separation

Declarations