NYLL
Module

NormImage.lean

Nyll.GaloisCohomology.Cyclic.TateH0.NormImage
12 declarations indexed from sourceView source ↗

Module documentation

Norm images in degree-zero Tate cohomology of units

The representation norm on the units of a field extension lands in the invariant units. Its image defines the norm submodule, and the quotient of the invariant units by this submodule realizes degree-zero Tate cohomology. The norm map is also compared with the field norm on units.

Imports5
Imported by8

Declarations

def

unitsNormLinearMap

L32 ↗
CyclicCohomology.unitsNormLinearMap
Documentation

The group-cohomological norm endomorphism on the actual unit representation.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
open CategoryTheory
noncomputable section
universe u
Lean source · statement
def unitsNormLinearMap (K L : Type) [Field K] [Field L] [Algebra K L]
    [Fintype Gal(L/K)] : Additive Lˣ →ₗ[ℤ] Additive Lˣ
lemma

unitsNorm_mem_invariants

L37 ↗
CyclicCohomology.unitsNorm_mem_invariants
Documentation

The additive unit norm is fixed by the Galois action.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
open CategoryTheory
noncomputable section
universe u
Lean source · statement
lemma unitsNorm_mem_invariants (K L : Type) [Field K] [Field L] [Algebra K L]
    [Fintype Gal(L/K)] (x : Additive Lˣ) :
    unitsNormLinearMap K L x ∈ unitsInvariantSubmodule K L
def

unitsNormToInvariantsLinearMap

L44 ↗
CyclicCohomology.unitsNormToInvariantsLinearMap
Documentation

The norm map, codomain-restricted to invariant units.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
open CategoryTheory
noncomputable section
universe u
Lean source · statement
def unitsNormToInvariantsLinearMap (K L : Type) [Field K] [Field L] [Algebra K L]
    [Fintype Gal(L/K)] : Additive Lˣ →ₗ[ℤ] unitsInvariantSubmodule K L
def

unitsTateH0NormSubmodule

L50 ↗
CyclicCohomology.unitsTateH0NormSubmodule
Documentation

Norm image inside invariant units.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
open CategoryTheory
noncomputable section
universe u
Lean source · statement
def unitsTateH0NormSubmodule (K L : Type) [Field K] [Field L] [Algebra K L]
    [Fintype Gal(L/K)] : Submodule ℤ (unitsInvariantSubmodule K L)
def

tateUnitsH0IsoInvariantsQuotient

L56 ↗
CyclicCohomology.tateUnitsH0IsoInvariantsQuotient
Documentation

The standard degree-zero Tate object, expressed as the arithmetic quotient of invariant units by the representation norm image.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
open CategoryTheory
noncomputable section
universe u
Lean source · statement
def tateUnitsH0IsoInvariantsQuotient (K L : Type)
    [Field K] [Field L] [Algebra K L] [Fintype Gal(L/K)] :
    tateCohomology (Rep.ofAlgebraAutOnUnits K L) 0 ≅
      ModuleCat.of ℤ
        (unitsInvariantSubmodule K L ⧸ unitsTateH0NormSubmodule K L)
theorem

unitsNormLinearMap_apply_val

L92 ↗
CyclicCohomology.unitsNormLinearMap_apply_val
Documentation

The value of the additive unit norm map is the field norm of the underlying unit.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
open CategoryTheory
noncomputable section
universe u
Lean source · full declaration
theorem unitsNormLinearMap_apply_val (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L] (x : Lˣ) :
    (letI := AlgEquiv.fintype K L
     (Additive.toMul (unitsNormLinearMap K L (Additive.ofMul x)) : Lˣ).1) =
      algebraMap K L (Algebra.norm K (x : L)) := by
  let := AlgEquiv.fintype K L
  dsimp only [unitsNormLinearMap]
  change ((Additive.toMul
    ((Rep.ofAlgebraAutOnUnits K L).norm.hom (Additive.ofMul x)) : Lˣ).1) =
      algebraMap K L (Algebra.norm K (x : L))
  rw [← groupCohomology.norm_ofAlgebraAutOnUnits_eq (K := K) (L := L) x]
  rfl
lemma

additive_toMul_finset_sum_units

L107 ↗
CyclicCohomology.additive_toMul_finset_sum_units
Documentation

A finite sum of additive units corresponds to the product of their underlying units.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
open CategoryTheory
noncomputable section
universe u
Lean source · full declaration
lemma additive_toMul_finset_sum_units {ι : Type*} (L : Type*) [Field L]
    (s : Finset ι) (f : ι → Additive Lˣ) :
    Additive.toMul (Finset.sum s f) =
      Finset.prod s (fun i => Additive.toMul (f i)) := by
  classical
  refine Finset.induction_on s ?h0 ?hstep
  · simp
  · intro a s ha hs
    simp [Finset.sum_insert, Finset.prod_insert, ha, hs]
def

additiveNormSubgroup

L118 ↗
CyclicCohomology.additiveNormSubgroup
Documentation

The additive subgroup of Additive Kˣ attached to the multiplicative norm subgroup.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
open CategoryTheory
noncomputable section
universe u
Lean source · statement
def additiveNormSubgroup (K L : Type u) [Field K] [Field L] [Algebra K L] :
    AddSubgroup (Additive Kˣ)
lemma

additiveNormSubgroup_eq_ker_quotient_map

L123 ↗
CyclicCohomology.additiveNormSubgroup_eq_ker_quotient_map
Documentation

The additive norm subgroup is the kernel of the norm-quotient map.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
open CategoryTheory
noncomputable section
universe u
Lean source · statement
lemma additiveNormSubgroup_eq_ker_quotient_map (K L : Type u)
    [Field K] [Field L] [Algebra K L] :
    additiveNormSubgroup K L =
      (MonoidHom.toAdditive (normClass K L)).ker
lemma

invariantsUnitsAddEquivBaseUnits_unitsNorm_apply

L141 ↗
CyclicCohomology.invariantsUnitsAddEquivBaseUnits_unitsNorm_apply
Documentation

The invariant-unit equivalence sends the additive unit norm to the field norm.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
open CategoryTheory
noncomputable section
universe u
Lean source · full declaration
lemma invariantsUnitsAddEquivBaseUnits_unitsNorm_apply (K L : Type)
    [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
    (x : Lˣ) :
    (letI := AlgEquiv.fintype K L
     invariantsUnitsAddEquivBaseUnits K L
        (unitsNormToInvariantsLinearMap K L (Additive.ofMul x))) =
      Additive.ofMul (normUnits K L x) := by
  let := AlgEquiv.fintype K L
  apply Additive.toMul.injective
  ext
  apply FaithfulSMul.algebraMap_injective K L
  rw [invariantsUnitsAddEquivBaseUnits_spec]
  exact (unitsNormLinearMap_apply_val K L x).trans (by rfl)
lemma

invariantsUnitsAddEquivBaseUnits_map_tateNormSubgroup

L156 ↗
CyclicCohomology.invariantsUnitsAddEquivBaseUnits_map_tateNormSubgroup
Documentation

The invariant-unit equivalence maps the Tate norm submodule onto the additive norm subgroup.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
open CategoryTheory
noncomputable section
universe u
Lean source · full declaration
lemma invariantsUnitsAddEquivBaseUnits_map_tateNormSubgroup (K L : Type)
    [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] :
    (letI := AlgEquiv.fintype K L
     (unitsTateH0NormSubmodule K L).toAddSubgroup.map
        (invariantsUnitsAddEquivBaseUnits K L).toAddMonoidHom) =
      additiveNormSubgroup K L := by
  let := AlgEquiv.fintype K L
  ext y
  constructor
  · rintro ⟨x, hx, rfl⟩
    rcases hx with ⟨z, rfl⟩
    change Additive.toMul
        (invariantsUnitsAddEquivBaseUnits K L
          (unitsNormToInvariantsLinearMap K L z)) ∈ localNormSubgroup K L
    let a : Lˣ := Additive.toMul z
    rw [show z = Additive.ofMul a by cases z; rfl]
    have hmap :=
      congrArg Additive.toMul
        (invariantsUnitsAddEquivBaseUnits_unitsNorm_apply K L a)
    rw [hmap]
    exact ⟨a, rfl⟩
  · intro hy
    change Additive.toMul y ∈ localNormSubgroup K L at hy
    rcases hy with ⟨x, hx⟩
    refine ⟨unitsNormToInvariantsLinearMap K L (Additive.ofMul x), ⟨Additive.ofMul x, rfl⟩, ?_⟩
    change
      invariantsUnitsAddEquivBaseUnits K L
          (unitsNormToInvariantsLinearMap K L (Additive.ofMul x)) = y
    calc
      invariantsUnitsAddEquivBaseUnits K L
          (unitsNormToInvariantsLinearMap K L (Additive.ofMul x))
          = Additive.ofMul (normUnits K L x) :=
            invariantsUnitsAddEquivBaseUnits_unitsNorm_apply K L x
      _ = Additive.ofMul (Additive.toMul y) := congrArg Additive.ofMul hx
      _ = y := by cases y; rfl
lemma

invariantsUnitsEquivBaseUnits_map_tateNormSubmodule

L193 ↗
CyclicCohomology.invariantsUnitsEquivBaseUnits_map_tateNormSubmodule
Documentation

The multiplicative invariant-unit equivalence maps Tate norms onto field norms.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
open CategoryTheory
noncomputable section
universe u
Lean source · full declaration
lemma invariantsUnitsEquivBaseUnits_map_tateNormSubmodule (K L : Type)
    [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] :
    (letI := AlgEquiv.fintype K L
     (unitsTateH0NormSubmodule K L).map
        (invariantsUnitsEquivBaseUnits K L : unitsInvariantSubmodule K L →ₗ[ℤ] Additive Kˣ)) =
      (additiveNormSubgroup K L).toIntSubmodule := by
  let := AlgEquiv.fintype K L
  apply Submodule.toAddSubgroup_injective
  rw [Submodule.map_toAddSubgroup]
  exact invariantsUnitsAddEquivBaseUnits_map_tateNormSubgroup K L

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