NYLL
Module

FractionFieldGalois.lean

Nyll.EtaleFundamentalGroups.Kummer.Lattices.FractionFieldGalois
3 declarations indexed from sourceView source ↗

Module documentation

Fraction-field Galois extension of a finite lattice cover

The quotient-character action on a lattice algebra extends canonically to its fraction field. The ring-level IsGaloisGroup producer and mathlib's fraction-ring transport then identify the same finite character group as a Galois group of the fraction-field extension.

Imports4
Imported by3

Declarations

theorem

latticeUniqueSums_of_freeIntModule

L30 ↗
EtaleFundamentalGroups.Kummer.latticeUniqueSums_of_freeIntModule
Documentation

A free abelian group has unique sums, via the coordinates of a chosen ℤ-basis. This is a named producer so lattice-algebra domain instances can remain local to fraction-field consumers.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v
Lean source · statement
theorem latticeUniqueSums_of_freeIntModule
    (L : Type v) [AddCommGroup L] [Module.Free ℤ L] : UniqueSums L
theorem

latticeSubgroupUniqueSums

L37 ↗
EtaleFundamentalGroups.Kummer.latticeSubgroupUniqueSums
Documentation

A subgroup of a unique-sums abelian group has unique sums.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v
Lean source · statement
theorem latticeSubgroupUniqueSums
    {L : Type v} [AddCommGroup L] [UniqueSums L] (H : AddSubgroup L) :
    UniqueSums H
theorem

latticeCharacter_isGaloisGroup_fractionRing

L48 ↗
EtaleFundamentalGroups.Kummer.latticeCharacter_isGaloisGroup_fractionRing
Documentation

The finite quotient-character group is a Galois group for the induced extension of lattice fraction fields. All actions and algebra structures are the named canonical producers from the ring-level lattice cover.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v
Lean source · full declaration
theorem latticeCharacter_isGaloisGroup_fractionRing
    {k : Type u} {L : Type v} [CommRing k] [IsDomain k]
    [AddCommGroup L]
    [Module.Free ℤ L]
    (H : AddSubgroup L) [Finite (L ⧸ H)]
    [HasEnoughRootsOfUnity k
      (Monoid.exponent (Multiplicative (L ⧸ H)))] :
    let A := AddMonoidAlgebra k H
    let B := AddMonoidAlgebra k L
    let G := Multiplicative (L ⧸ H) →* kˣ
    letI : UniqueSums L := latticeUniqueSums_of_freeIntModule L
    letI : UniqueSums H := latticeSubgroupUniqueSums H
    letI : IsDomain A := inferInstance
    letI : IsDomain B := inferInstance
    letI : Algebra A B := latticeMapDomainAlgebra H
    letI : FaithfulSMul A B := latticeMapDomainFaithfulSMul H
    let K := FractionRing A
    let E := FractionRing B
    letI : Algebra K E := FractionRing.liftAlgebra A E
    letI : MulSemiringAction G B := latticeCharacterMulSemiringAction H
    letI : MulSemiringAction G E := IsFractionRing.mulSemiringAction G B E
    IsGaloisGroup G K E := by
  dsimp only
  let A := AddMonoidAlgebra k H
  let B := AddMonoidAlgebra k L
  let G := Multiplicative (L ⧸ H) →* kˣ
  let K := FractionRing A
  let E := FractionRing B
  let : UniqueSums L := latticeUniqueSums_of_freeIntModule L
  let : UniqueSums H := latticeSubgroupUniqueSums H
  let : IsDomain A := inferInstance
  let : IsDomain B := inferInstance
  let : Algebra A B := latticeMapDomainAlgebra H
  let : FaithfulSMul A B := latticeMapDomainFaithfulSMul H
  let : Algebra K E := FractionRing.liftAlgebra A E
  let : MulSemiringAction G B := latticeCharacterMulSemiringAction H
  let : MulSemiringAction G E := IsFractionRing.mulSemiringAction G B E
  let : Finite G := latticeCharacterGroupFinite H
  have : IsGaloisGroup G A B := latticeCharacter_isGaloisGroup H
  infer_instance

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.