Module

GaloisGroup.lean

Nyll.EtaleFundamentalGroups.Kummer.Lattices.GaloisGroup

6 declarations indexed from sourceView source ↗

Module documentation

Galois group of a finite lattice cover

The character group of the finite quotient lattice acts diagonally on the ambient lattice algebra. This file packages that already constructed action as a local MulSemiringAction, equips the lattice cover with its canonical map-domain algebra structure, and proves that the character group is the Galois group in the sense of IsGaloisGroup.

The action, algebra structure, and finiteness proof are named definitions, not global instances. This lets fraction-field consumers reuse exactly the same action while keeping instance search local.

Imports3

Mathlib.Algebra.Algebra.Basic
Mathlib.RingTheory.IsGaloisGroup.Defs
Nyll.EtaleFundamentalGroups.Kummer.Lattices.CharacterAction

Imported by2

def

latticeCharacterMulSemiringAction

L33 ↗

EtaleFundamentalGroups.Kummer.latticeCharacterMulSemiringAction

Documentation

The local semiring action induced by the diagonal character action.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u v
noncomputable section

Lean source · statement

def latticeCharacterMulSemiringAction
    {k : Type u} {L : Type v} [CommRing k] [AddCommGroup L]
    (H : AddSubgroup L) :
    MulSemiringAction (Multiplicative (L ⧸ H) →* kˣ)
      (AddMonoidAlgebra k L)

def

latticeMapDomainAlgebra

L44 ↗

EtaleFundamentalGroups.Kummer.latticeMapDomainAlgebra

Documentation

The canonical algebra structure on a lattice cover, induced by the map-domain homomorphism of the subgroup inclusion.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u v
noncomputable section

Lean source · statement

def latticeMapDomainAlgebra
    {k : Type u} {L : Type v} [CommRing k] [AddCommGroup L]
    (H : AddSubgroup L) :
    Algebra (AddMonoidAlgebra k H) (AddMonoidAlgebra k L)

theorem

latticeMapDomainFaithfulSMul

L52 ↗

EtaleFundamentalGroups.Kummer.latticeMapDomainFaithfulSMul

Documentation

The map-domain algebra structure is faithful because the subgroup inclusion, hence the induced map of lattice algebras, is injective.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u v
noncomputable section

Lean source · full declaration

theorem latticeMapDomainFaithfulSMul
    {k : Type u} {L : Type v} [CommRing k] [AddCommGroup L]
    (H : AddSubgroup L) :
    letI := latticeMapDomainAlgebra (k := k) H
    FaithfulSMul (AddMonoidAlgebra k H) (AddMonoidAlgebra k L) := by
  let := latticeMapDomainAlgebra (k := k) H
  rw [faithfulSMul_iff_algebraMap_injective]
  change Function.Injective (AddMonoidAlgebra.mapDomain H.subtype)
  exact AddMonoidAlgebra.mapDomain_injective H.subtype_injective

theorem

latticeCharacterAction_injective

L64 ↗

EtaleFundamentalGroups.Kummer.latticeCharacterAction_injective

Documentation

Distinct quotient characters induce distinct diagonal automorphisms of the ambient lattice algebra.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u v
noncomputable section

Lean source · statement

theorem latticeCharacterAction_injective
    {k : Type u} {L : Type v} [CommRing k] [AddCommGroup L]
    (H : AddSubgroup L) :
    Function.Injective (latticeCharacterAction (k := k) H)

theorem

latticeCharacterGroupFinite

L77 ↗

EtaleFundamentalGroups.Kummer.latticeCharacterGroupFinite

Documentation

The character group is finite. This is kept as a named producer so it can be installed only by fraction-field consumers of the Galois action.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u v
noncomputable section

Lean source · statement

theorem latticeCharacterGroupFinite
    {k : Type u} {L : Type v} [CommRing k] [AddCommGroup L]
    (H : AddSubgroup L) [Finite (L ⧸ H)]
    [HasEnoughRootsOfUnity k
      (Monoid.exponent (Multiplicative (L ⧸ H)))] :
    Finite (Multiplicative (L ⧸ H) →* kˣ)

theorem

latticeCharacter_isGaloisGroup

L90 ↗

EtaleFundamentalGroups.Kummer.latticeCharacter_isGaloisGroup

Documentation

The diagonal quotient-character action makes the finite lattice cover a Galois extension. Both structures used by IsGaloisGroup are local and are reproducible from the named action and map-domain algebra definitions above.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u v
noncomputable section

Lean source · full declaration

theorem latticeCharacter_isGaloisGroup
    {k : Type u} {L : Type v} [CommRing k] [IsDomain k]
    [AddCommGroup L]
    (H : AddSubgroup L) [Finite (L ⧸ H)]
    [HasEnoughRootsOfUnity k
      (Monoid.exponent (Multiplicative (L ⧸ H)))] :
    letI := latticeCharacterMulSemiringAction (k := k) H
    letI := latticeMapDomainAlgebra (k := k) H
    IsGaloisGroup (Multiplicative (L ⧸ H) →* kˣ)
      (AddMonoidAlgebra k H) (AddMonoidAlgebra k L) := by
  let := latticeCharacterMulSemiringAction (k := k) H
  let := latticeMapDomainAlgebra (k := k) H
  have hfixed :
      {x : AddMonoidAlgebra k L |
          ∀ χ : Multiplicative (L ⧸ H) →* kˣ,
            latticeCharacterAction H χ x = x} =
        ((AddMonoidAlgebra.mapDomainAlgHom k k H.subtype).range :
          Set (AddMonoidAlgebra k L)) :=
    fixedBy_latticeCharacterAction_eq_range (k := k) H
  refine
    { faithful := ?_
      commutes := ?_
      isInvariant := ?_ }
  · refine ⟨?_⟩
    intro χ ψ hχψ
    apply latticeCharacterAction_injective (k := k) H
    exact AlgEquiv.ext fun x => hχψ x
  · refine ⟨?_⟩
    intro χ a b
    have ha :
        latticeCharacterAction H χ
            (AddMonoidAlgebra.mapDomainAlgHom k k H.subtype a) =
          AddMonoidAlgebra.mapDomainAlgHom k k H.subtype a := by
      have haRange :
          AddMonoidAlgebra.mapDomainAlgHom k k H.subtype a ∈
            ((AddMonoidAlgebra.mapDomainAlgHom k k H.subtype).range :
              Set (AddMonoidAlgebra k L)) :=
        ⟨a, rfl⟩
      rw [← hfixed] at haRange
      exact haRange χ
    rw [Algebra.smul_def, Algebra.smul_def]
    change latticeCharacterAction H χ
        (AddMonoidAlgebra.mapDomainAlgHom k k H.subtype a * b) =
      AddMonoidAlgebra.mapDomainAlgHom k k H.subtype a *
        latticeCharacterAction H χ b
    rw [map_mul, ha]
  · refine ⟨?_⟩
    intro b hb
    have hbFixed :
        b ∈ {x : AddMonoidAlgebra k L |
          ∀ χ : Multiplicative (L ⧸ H) →* kˣ,
            latticeCharacterAction H χ x = x} := by
      intro χ
      exact hb χ
    rw [hfixed] at hbFixed
    obtain ⟨a, ha⟩ := hbFixed
    refine ⟨a, ?_⟩
    change AddMonoidAlgebra.mapDomainAlgHom k k H.subtype a = b
    exact ha

Module documentation

Galois group of a finite lattice cover

Declarations

latticeCharacterMulSemiringAction

latticeMapDomainAlgebra

latticeMapDomainFaithfulSMul

latticeCharacterAction_injective

latticeCharacterGroupFinite

latticeCharacter_isGaloisGroup