Module

Invariants.lean

Nyll.GaloisCohomology.Cyclic.TateH0.Invariants

9 declarations indexed from sourceView source ↗

Module documentation

Invariant units

The actual invariant submodule of the unit representation, together with its arithmetic identification with the units of the base field.

Imports2

Mathlib.RepresentationTheory.Invariants
Mathlib.FieldTheory.Galois.Basic

Imported by5

def

unitsInvariantSubmodule

L22 ↗

CyclicCohomology.unitsInvariantSubmodule

Documentation

The actual invariant submodule of the unit representation Lˣ under Gal(L/K).

Source context 2 commands

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

namespace CyclicCohomology
noncomputable section

Lean source · statement

def unitsInvariantSubmodule (K L : Type) [Field K] [Field L] [Algebra K L] :
    Submodule ℤ (Additive Lˣ)

def

invariantUnitToBaseUnit

L26 ↗

CyclicCohomology.invariantUnitToBaseUnit

Source context 2 commands

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

namespace CyclicCohomology
noncomputable section

Lean source · statement

def invariantUnitToBaseUnit (K L : Type)
    [Field K] [Field L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L]
    (x : unitsInvariantSubmodule K L) : Kˣ

lemma

invariantUnitToBaseUnit_spec

L51 ↗

CyclicCohomology.invariantUnitToBaseUnit_spec

Source context 2 commands

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

namespace CyclicCohomology
noncomputable section

Lean source · statement

lemma invariantUnitToBaseUnit_spec (K L : Type)
    [Field K] [Field L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L]
    (x : unitsInvariantSubmodule K L) :
    algebraMap K L (invariantUnitToBaseUnit K L x : K) =
      ((Additive.toMul (x : Additive Lˣ) : Lˣ) : L)

def

baseUnitToInvariantUnit

L74 ↗

CyclicCohomology.baseUnitToInvariantUnit

Source context 2 commands

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

namespace CyclicCohomology
noncomputable section

Lean source · full declaration

def baseUnitToInvariantUnit (K L : Type)
    [Field K] [Field L] [Algebra K L] (x : Kˣ) : unitsInvariantSubmodule K L where
  val := Additive.ofMul (Units.map (algebraMap K L).toMonoidHom x)
  property := by
    intro σ
    change
      Additive.ofMul
          (Units.mapEquiv σ.toMulEquiv (Units.map (algebraMap K L).toMonoidHom x)) =
        Additive.ofMul (Units.map (algebraMap K L).toMonoidHom x)
    apply Additive.ofMul.injective
    ext
    simp

lemma

invariantUnitToBaseUnit_baseUnitToInvariantUnit

L87 ↗

CyclicCohomology.invariantUnitToBaseUnit_baseUnitToInvariantUnit

Source context 2 commands

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

namespace CyclicCohomology
noncomputable section

Lean source · statement

lemma invariantUnitToBaseUnit_baseUnitToInvariantUnit (K L : Type)
    [Field K] [Field L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L]
    (x : Kˣ) :
    invariantUnitToBaseUnit K L (baseUnitToInvariantUnit K L x) = x

lemma

baseUnitToInvariantUnit_invariantUnitToBaseUnit

L96 ↗

CyclicCohomology.baseUnitToInvariantUnit_invariantUnitToBaseUnit

Source context 2 commands

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

namespace CyclicCohomology
noncomputable section

Lean source · statement

lemma baseUnitToInvariantUnit_invariantUnitToBaseUnit (K L : Type)
    [Field K] [Field L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L]
    (x : unitsInvariantSubmodule K L) :
    baseUnitToInvariantUnit K L (invariantUnitToBaseUnit K L x) = x

def

invariantsUnitsAddEquivBaseUnits

L106 ↗

CyclicCohomology.invariantsUnitsAddEquivBaseUnits

Documentation

The canonical additive equivalence (Lˣ)^Gal(L/K) ≃ Kˣ for finite Galois extensions.

Source context 2 commands

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

namespace CyclicCohomology
noncomputable section

Lean source · full declaration

def invariantsUnitsAddEquivBaseUnits (K L : Type)
    [Field K] [Field L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] :
    unitsInvariantSubmodule K L ≃+ Additive Kˣ where
  toFun := fun x => Additive.ofMul (invariantUnitToBaseUnit K L x)
  invFun := fun x => baseUnitToInvariantUnit K L (Additive.toMul x)
  left_inv := baseUnitToInvariantUnit_invariantUnitToBaseUnit K L
  right_inv := by
    intro x
    apply Additive.ofMul.injective
    exact invariantUnitToBaseUnit_baseUnitToInvariantUnit K L (Additive.toMul x)
  map_add' := by
    intro x y
    apply Additive.ofMul.injective
    change
      invariantUnitToBaseUnit K L (x + y) =
        invariantUnitToBaseUnit K L x * invariantUnitToBaseUnit K L y
    ext
    apply FaithfulSMul.algebraMap_injective K L
    change
      algebraMap K L (invariantUnitToBaseUnit K L (x + y) : K) =
        algebraMap K L
          ((invariantUnitToBaseUnit K L x : K) *
            (invariantUnitToBaseUnit K L y : K))
    rw [map_mul, invariantUnitToBaseUnit_spec,
      invariantUnitToBaseUnit_spec, invariantUnitToBaseUnit_spec]
    rfl

def

invariantsUnitsEquivBaseUnits

L134 ↗

CyclicCohomology.invariantsUnitsEquivBaseUnits

Documentation

The canonical linear equivalence (Lˣ)^Gal(L/K) ≃ Kˣ for finite Galois extensions.

Source context 2 commands

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

namespace CyclicCohomology
noncomputable section

Lean source · statement

def invariantsUnitsEquivBaseUnits (K L : Type)
    [Field K] [Field L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] :
    unitsInvariantSubmodule K L ≃ₗ[ℤ] Additive Kˣ

lemma

invariantsUnitsAddEquivBaseUnits_spec

L141 ↗

CyclicCohomology.invariantsUnitsAddEquivBaseUnits_spec

Documentation

Restricting an invariant unit and re-embedding its value recovers the underlying extension-field unit.

Source context 2 commands

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

namespace CyclicCohomology
noncomputable section

Lean source · statement

lemma invariantsUnitsAddEquivBaseUnits_spec (K L : Type)
    [Field K] [Field L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L]
    (x : unitsInvariantSubmodule K L) :
    algebraMap K L
        ((Additive.toMul (invariantsUnitsAddEquivBaseUnits K L x) : Kˣ) : K) =
      ((Additive.toMul (x : Additive Lˣ) : Lˣ) : L)

Module documentation

Invariant units

Declarations