NYLL
Module

FiniteGaloisTowerUnitsH2.lean

Nyll.GaloisCohomology.Kummer.FiniteGaloisTowerUnitsH2
9 declarations indexed from sourceView source ↗

Module documentation

Unit H² in an arbitrary finite Galois tower

The actual restriction homomorphisms and inclusion of units define the inflation and restriction maps without representing the lower field as a subtype of the upper field.

Imports14
Imported by5

Declarations

def

finiteGaloisTowerUnitsInflationRepHom

L40 ↗
ClassFieldTower.Cohomology.finiteGaloisTowerUnitsInflationRepHom
Documentation

Inclusion of units in a normal field tower, equivariant for restriction.

Source context 4 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K F N : Type) [Field K] [Field F] [Field N]
  [Algebra K F] [Algebra F N] [Algebra K N] [IsScalarTower K F N]
Lean source · statement
def finiteGaloisTowerUnitsInflationRepHom [Normal K F] :
    Rep.res (AlgEquiv.restrictNormalHom F) (Rep.ofAlgebraAutOnUnits K F) ⟶
      Rep.ofAlgebraAutOnUnits K N
def

finiteGaloisTowerUnitsH2Inflation

L52 ↗
ClassFieldTower.Cohomology.finiteGaloisTowerUnitsH2Inflation
Documentation

Inflation induced by restricting automorphisms and including field units.

Source context 4 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K F N : Type) [Field K] [Field F] [Field N]
  [Algebra K F] [Algebra F N] [Algebra K N] [IsScalarTower K F N]
Lean source · statement
def finiteGaloisTowerUnitsH2Inflation [Normal K F] :
    groupCohomology (Rep.ofAlgebraAutOnUnits K F) 2 ⟶
      groupCohomology (Rep.ofAlgebraAutOnUnits K N) 2
def

finiteGaloisTowerUnitsRestrictionRepHom

L59 ↗
ClassFieldTower.Cohomology.finiteGaloisTowerUnitsRestrictionRepHom
Documentation

Relative restriction leaves upper-field units unchanged.

Source context 4 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K F N : Type) [Field K] [Field F] [Field N]
  [Algebra K F] [Algebra F N] [Algebra K N] [IsScalarTower K F N]
Lean source · statement
def finiteGaloisTowerUnitsRestrictionRepHom :
    Rep.res (AlgEquiv.restrictScalarsHom K) (Rep.ofAlgebraAutOnUnits K N) ⟶
      Rep.ofAlgebraAutOnUnits F N
def

finiteGaloisTowerUnitsH2Restriction

L65 ↗
ClassFieldTower.Cohomology.finiteGaloisTowerUnitsH2Restriction
Documentation

Restriction to the relative Galois group, with identical unit coefficients.

Source context 4 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K F N : Type) [Field K] [Field F] [Field N]
  [Algebra K F] [Algebra F N] [Algebra K N] [IsScalarTower K F N]
Lean source · statement
def finiteGaloisTowerUnitsH2Restriction :
    groupCohomology (Rep.ofAlgebraAutOnUnits K N) 2 ⟶
      groupCohomology (Rep.ofAlgebraAutOnUnits F N) 2
theorem

restriction_intermediateField

L71 ↗
ClassFieldTower.Cohomology.restriction_intermediateField
Source context 4 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K F N : Type) [Field K] [Field F] [Field N]
  [Algebra K F] [Algebra F N] [Algebra K N] [IsScalarTower K F N]
Lean source · statement
theorem restriction_intermediateField (E : IntermediateField K N) :
    finiteGaloisUnitsH2Restriction K N E =
      finiteGaloisTowerUnitsH2Restriction K E N
theorem

fieldRange_inflation

L94 ↗
ClassFieldTower.Cohomology.fieldRange_inflation
Source context 4 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K F N : Type) [Field K] [Field F] [Field N]
  [Algebra K F] [Algebra F N] [Algebra K N] [IsScalarTower K F N]
Lean source · statement
theorem fieldRange_inflation [Normal K F]
    [Normal K (IsScalarTower.toAlgHom K F N).fieldRange] :
    (unitsCohomologyCongrTop K F (IsScalarTower.toAlgHom K F N).fieldRange
      (IsScalarTower.toAlgHom K F N).equivFieldRange 2).hom ≫
        finiteGaloisUnitsH2Inflation K N (IsScalarTower.toAlgHom K F N).fieldRange =
      finiteGaloisTowerUnitsH2Inflation K F N
theorem

finiteGaloisTowerUnitsH2Inflation_injective

L138 ↗
ClassFieldTower.Cohomology.finiteGaloisTowerUnitsH2Inflation_injective
Documentation

Field-unit inflation is injective for an arbitrary finite Galois tower.

Source context 4 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K F N : Type) [Field K] [Field F] [Field N]
  [Algebra K F] [Algebra F N] [Algebra K N] [IsScalarTower K F N]
Lean source · statement
theorem finiteGaloisTowerUnitsH2Inflation_injective
    [Normal K F] [FiniteDimensional K N] [IsGalois K N] :
    Function.Injective (finiteGaloisTowerUnitsH2Inflation K F N).hom
theorem

restriction_surjectiveScalars

L151 ↗
ClassFieldTower.Cohomology.restriction_surjectiveScalars
Source context 4 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K F N : Type) [Field K] [Field F] [Field N]
  [Algebra K F] [Algebra F N] [Algebra K N] [IsScalarTower K F N]
Lean source · statement
theorem restriction_surjectiveScalars
    (E : Type) [Field E] [Algebra K E] [Algebra E N] [IsScalarTower K E N]
    [Algebra F E] [IsScalarTower F E N]
    (h : Function.Surjective (algebraMap F E)) :
    finiteGaloisTowerUnitsH2Restriction K E N ≫
      (unitsCohomologyRestrictScalarsIso F E N h 2).hom =
        finiteGaloisTowerUnitsH2Restriction K F N
theorem

finiteGaloisTowerUnitsH2Restriction_ker_le_inflation_range

L177 ↗
ClassFieldTower.Cohomology.finiteGaloisTowerUnitsH2Restriction_ker_le_inflation_range
Documentation

Middle exactness for unit H² in an arbitrary finite Galois tower.

Source context 4 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K F N : Type) [Field K] [Field F] [Field N]
  [Algebra K F] [Algebra F N] [Algebra K N] [IsScalarTower K F N]
Lean source · statement
theorem finiteGaloisTowerUnitsH2Restriction_ker_le_inflation_range
    [Normal K F] [FiniteDimensional K N] [IsGalois K N] :
    (finiteGaloisTowerUnitsH2Restriction K F N).hom.ker ≤
      (finiteGaloisTowerUnitsH2Inflation K F N).hom.range

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