Module

FiniteGaloisUnitsH2Inflation.lean

Nyll.GaloisCohomology.Kummer.FiniteGaloisUnitsH2Inflation

13 declarations indexed from sourceView source ↗

Module documentation

Injectivity of field-unit H² inflation

The map is induced by actual restriction to a normal intermediate field and inclusion of its units. For a finite Galois upper field, Hilbert 90 corrects an upper primitive by an actual principal one-coboundary. The corrected primitive is constant on restriction fibres and its values are fixed by all relative automorphisms, so it descends to the lower field.

Imports11

Mathlib.FieldTheory.Galois.Basic
Mathlib.FieldTheory.Normal.Basic
Mathlib.FieldTheory.Normal.Defs
Mathlib.FieldTheory.IntermediateField.Basic
Mathlib.Algebra.Group.Units.Hom
Mathlib.RepresentationTheory.Rep.Basic
Mathlib.RepresentationTheory.Rep.Res
Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Mathlib.Tactic.Abel

Imported by5

def

unitsInclusion

L38 ↗

ClassFieldTower.Cohomology.unitsInclusion

Source context 5 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (E : IntermediateField K L) [Normal K E]

Lean source · statement

def unitsInclusion :
    Rep.ofAlgebraAutOnUnits K E →+ Rep.ofAlgebraAutOnUnits K L

theorem

unitsInclusion_injective

L43 ↗

ClassFieldTower.Cohomology.unitsInclusion_injective

Source context 6 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (E : IntermediateField K L) [Normal K E]
omit [Normal K E] in

Lean source · statement

theorem unitsInclusion_injective : Function.Injective (unitsInclusion K L E)

theorem

unitsInclusion_equivariant

L46 ↗

ClassFieldTower.Cohomology.unitsInclusion_equivariant

Source context 5 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (E : IntermediateField K L) [Normal K E]

Lean source · statement

theorem unitsInclusion_equivariant (σ : Gal(L/K)) (a : Rep.ofAlgebraAutOnUnits K E) :
    unitsInclusion K L E ((Rep.ofAlgebraAutOnUnits K E).ρ
      (AlgEquiv.restrictNormalHom E σ) a) =
      (Rep.ofAlgebraAutOnUnits K L).ρ σ (unitsInclusion K L E a)

def

finiteGaloisUnitsInflationRepHom

L55 ↗

ClassFieldTower.Cohomology.finiteGaloisUnitsInflationRepHom

Documentation

The actual inclusion of lower-field units, equivariant for restriction of the upper Galois group to the normal intermediate field.

Source context 5 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (E : IntermediateField K L) [Normal K E]

Lean source · statement

def finiteGaloisUnitsInflationRepHom :
    Rep.res (AlgEquiv.restrictNormalHom E)
      (Rep.ofAlgebraAutOnUnits K E) ⟶ Rep.ofAlgebraAutOnUnits K L

def

finiteGaloisUnitsH2Inflation

L67 ↗

ClassFieldTower.Cohomology.finiteGaloisUnitsH2Inflation

Documentation

Inflation with the actual field-unit coefficient inclusion in a finite Galois tower.

Source context 5 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (E : IntermediateField K L) [Normal K E]

Lean source · statement

def finiteGaloisUnitsH2Inflation :
    groupCohomology (Rep.ofAlgebraAutOnUnits K E) 2 ⟶
      groupCohomology (Rep.ofAlgebraAutOnUnits K L) 2

theorem

restrictNormal_restrictScalars

L73 ↗

ClassFieldTower.Cohomology.restrictNormal_restrictScalars

Source context 5 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (E : IntermediateField K L) [Normal K E]

Lean source · statement

theorem restrictNormal_restrictScalars (τ : Gal(L/E)) :
    AlgEquiv.restrictNormalHom E (τ.restrictScalars K) = 1

theorem

unitsInclusion_relative_fixed

L80 ↗

ClassFieldTower.Cohomology.unitsInclusion_relative_fixed

Source context 6 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (E : IntermediateField K L) [Normal K E]
omit [Normal K E] in

Lean source · statement

theorem unitsInclusion_relative_fixed (τ : Gal(L/E)) (a : Rep.ofAlgebraAutOnUnits K E) :
    (Rep.ofAlgebraAutOnUnits K L).ρ (τ.restrictScalars K) (unitsInclusion K L E a) =
      unitsInclusion K L E a

theorem

exists_relativeAut_of_restrictNormal_eq_one

L86 ↗

ClassFieldTower.Cohomology.exists_relativeAut_of_restrictNormal_eq_one

Source context 5 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (E : IntermediateField K L) [Normal K E]

Lean source · statement

theorem exists_relativeAut_of_restrictNormal_eq_one
    (σ : Gal(L/K)) (hσ : AlgEquiv.restrictNormalHom E σ = 1) :
    ∃ τ : Gal(L/E), τ.restrictScalars K = σ

theorem

exists_unitsInclusion_eq_of_fixed

L97 ↗

ClassFieldTower.Cohomology.exists_unitsInclusion_eq_of_fixed

Source context 7 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (E : IntermediateField K L) [Normal K E]
variable [FiniteDimensional K L] [IsGalois K L]
omit [Normal K E] in

Lean source · statement

theorem exists_unitsInclusion_eq_of_fixed (a : Rep.ofAlgebraAutOnUnits K L)
    (ha : ∀ τ : Gal(L/E), (Rep.ofAlgebraAutOnUnits K L).ρ (τ.restrictScalars K) a = a) :
    ∃ b : Rep.ofAlgebraAutOnUnits K E, unitsInclusion K L E b = a

theorem

exists_primitive_constant_on_relativeAut

L115 ↗

ClassFieldTower.Cohomology.exists_primitive_constant_on_relativeAut

Source context 7 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (E : IntermediateField K L) [Normal K E]
variable [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem exists_primitive_constant_on_relativeAut
    (c : groupCohomology.cocycles₂ (Rep.ofAlgebraAutOnUnits K E))
    (b : Gal(L/K) → Rep.ofAlgebraAutOnUnits K L)
    (hb : ∀ σ τ : Gal(L/K),
      (Rep.ofAlgebraAutOnUnits K L).ρ σ (b τ) - b (σ * τ) + b σ =
        unitsInclusion K L E
          (c (AlgEquiv.restrictNormalHom E σ, AlgEquiv.restrictNormalHom E τ))) :
    ∃ b' : Gal(L/K) → Rep.ofAlgebraAutOnUnits K L,
      (∀ σ τ : Gal(L/K),
        (Rep.ofAlgebraAutOnUnits K L).ρ σ (b' τ) - b' (σ * τ) + b' σ =
          unitsInclusion K L E
            (c (AlgEquiv.restrictNormalHom E σ, AlgEquiv.restrictNormalHom E τ))) ∧
      ∀ τ : Gal(L/E), b' (τ.restrictScalars K) = b' 1

theorem

exists_lower_primitive

L172 ↗

ClassFieldTower.Cohomology.exists_lower_primitive

Source context 6 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (E : IntermediateField K L) [Normal K E]
variable [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem exists_lower_primitive
    (c : groupCohomology.cocycles₂ (Rep.ofAlgebraAutOnUnits K E))
    (b : Gal(L/K) → Rep.ofAlgebraAutOnUnits K L)
    (hb : ∀ σ τ : Gal(L/K),
      (Rep.ofAlgebraAutOnUnits K L).ρ σ (b τ) - b (σ * τ) + b σ =
        unitsInclusion K L E
          (c (AlgEquiv.restrictNormalHom E σ, AlgEquiv.restrictNormalHom E τ)))
    (hn : ∀ τ : Gal(L/E), b (τ.restrictScalars K) = b 1) :
    ∃ a : Gal(E/K) → Rep.ofAlgebraAutOnUnits K E,
      groupCohomology.d₁₂ (Rep.ofAlgebraAutOnUnits K E) a = c

theorem

finiteGaloisUnitsH2Inflation_H2π

L240 ↗

ClassFieldTower.Cohomology.finiteGaloisUnitsH2Inflation_H2π

Documentation

Inflation sends an actual two-cocycle class to the class obtained by restricting its arguments and including its field-unit values.

Source context 7 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (E : IntermediateField K L) [Normal K E]
variable [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem finiteGaloisUnitsH2Inflation_H2π
    (c : groupCohomology.cocycles₂ (Rep.ofAlgebraAutOnUnits K E)) :
    (finiteGaloisUnitsH2Inflation K L E).hom
        (groupCohomology.H2π (Rep.ofAlgebraAutOnUnits K E) c) =
      groupCohomology.H2π (Rep.ofAlgebraAutOnUnits K L)
        (groupCohomology.mapCocycles₂ (AlgEquiv.restrictNormalHom E)
          (finiteGaloisUnitsInflationRepHom K L E) c)

theorem

finiteGaloisUnitsH2Inflation_injective

L254 ↗

ClassFieldTower.Cohomology.finiteGaloisUnitsH2Inflation_injective

Documentation

Inflation on actual field-unit H² is injective in a finite Galois tower. Noether–Hilbert90 corrects any upper primitive so that it descends to a lower-field primitive.

Source context 6 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable (E : IntermediateField K L) [Normal K E]
variable [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem finiteGaloisUnitsH2Inflation_injective :
    Function.Injective (finiteGaloisUnitsH2Inflation K L E).hom

Module documentation

Injectivity of field-unit H² inflation

Declarations