NYLL
Module

FiniteGaloisUnitsCohomologyTransport.lean

Nyll.GaloisCohomology.Kummer.FiniteGaloisUnitsCohomologyTransport
13 declarations indexed from sourceView source ↗

Module documentation

Transport of finite Galois field-unit cohomology

Identifies the invariant and quotient representations associated to an intermediate field and transports the degree-two inflation and restriction maps.

Imports17
  • Nyll.GaloisCohomology.Kummer.FiniteGaloisUnitsH2Inflation
  • Nyll.GaloisCohomology.Kummer.QuotientTwoCocycle
  • Mathlib.Algebra.Category.ModuleCat.Basic
  • Mathlib.Algebra.Group.Units.Hom
  • Mathlib.Algebra.Module.Submodule.Equiv
  • Mathlib.Algebra.Module.Submodule.LinearMap
  • Mathlib.FieldTheory.IntermediateField.Basic
  • Mathlib.RepresentationTheory.Rep.Basic
  • Mathlib.RepresentationTheory.Rep.Res
  • Mathlib.FieldTheory.Galois.Basic
  • Mathlib.FieldTheory.Normal.Basic
  • Mathlib.FieldTheory.Normal.Defs
  • Mathlib.GroupTheory.QuotientGroup.Basic
  • Mathlib.GroupTheory.QuotientGroup.Defs
  • Mathlib.RepresentationTheory.Invariants
  • Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
  • Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
Imported by6

Declarations

def

finiteGaloisUnitsRelativeCohomologyIso

L43 ↗
ClassFieldTower.Cohomology.finiteGaloisUnitsRelativeCohomologyIso
Documentation

Restriction to the fixing subgroup uses the actual relative automorphism action on the same field units.

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)
Lean source · statement
def finiteGaloisUnitsRelativeCohomologyIso (n : ℕ) :
    groupCohomology (Rep.res E.fixingSubgroup.subtype (Rep.ofAlgebraAutOnUnits K L)) n ≅
      groupCohomology (Rep.ofAlgebraAutOnUnits E L) n
theorem

finiteGaloisUnitsFixingSubgroupH1_subsingleton

L52 ↗
ClassFieldTower.Cohomology.finiteGaloisUnitsFixingSubgroupH1_subsingleton
Documentation

Hilbert 90 for the actual fixing-subgroup representation.

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)
variable [FiniteDimensional K L]
Lean source · statement
theorem finiteGaloisUnitsFixingSubgroupH1_subsingleton :
    Subsingleton (groupCohomology
      (Rep.res E.fixingSubgroup.subtype (Rep.ofAlgebraAutOnUnits K L)) 1)
def

unitsToInvariants

L57 ↗
ClassFieldTower.Cohomology.unitsToInvariants
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)
variable [FiniteDimensional K L]
Lean source · statement
def unitsToInvariants :
    Rep.ofAlgebraAutOnUnits K E →ₗ[ℤ]
      (Rep.res E.fixingSubgroup.subtype (Rep.ofAlgebraAutOnUnits K L)).ρ.invariants
theorem

unitsToInvariants_bijective

L67 ↗
ClassFieldTower.Cohomology.unitsToInvariants_bijective
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)
variable [FiniteDimensional K L]
variable [IsGalois K L]
Lean source · statement
theorem unitsToInvariants_bijective : Function.Bijective (unitsToInvariants K L E)
def

finiteGaloisUnitsInvariantsEquiv

L89 ↗
ClassFieldTower.Cohomology.finiteGaloisUnitsInvariantsEquiv
Documentation

The lower-field units are precisely the upper-field units fixed by the actual relative automorphisms.

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)
variable [FiniteDimensional K L]
variable [IsGalois K L]
Lean source · statement
def finiteGaloisUnitsInvariantsEquiv :
    (Rep.ofAlgebraAutOnUnits K E).V ≃ₗ[ℤ]
      (Rep.res E.fixingSubgroup.subtype (Rep.ofAlgebraAutOnUnits K L)).ρ.invariants
def

restrictionQuotientEquiv

L96 ↗
ClassFieldTower.Cohomology.restrictionQuotientEquiv
Source context 8 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)
variable [FiniteDimensional K L]
variable [IsGalois K L]
variable [Normal K E]
Lean source · statement
def restrictionQuotientEquiv :
    Gal(L/K) ⧸ (AlgEquiv.restrictNormalHom (F := K) (K₁ := L) E).ker ≃* Gal(E/K)
def

unitsToKernelInvariantsEquiv

L101 ↗
ClassFieldTower.Cohomology.unitsToKernelInvariantsEquiv
Source context 8 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)
variable [FiniteDimensional K L]
variable [IsGalois K L]
variable [Normal K E]
Lean source · statement
def unitsToKernelInvariantsEquiv :
    (Rep.ofAlgebraAutOnUnits K E).V ≃ₗ[ℤ]
      ((Rep.ofAlgebraAutOnUnits K L).quotientToInvariants
        (AlgEquiv.restrictNormalHom (F := K) (K₁ := L) E).ker).V
theorem

unitsInvariants_equivariant

L108 ↗
ClassFieldTower.Cohomology.unitsInvariants_equivariant
Source context 8 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)
variable [FiniteDimensional K L]
variable [IsGalois K L]
variable [Normal K E]
Lean source · statement
theorem unitsInvariants_equivariant (g : Gal(E/K)) :
    (unitsToKernelInvariantsEquiv K L E).toLinearMap ∘ₗ
        (Rep.ofAlgebraAutOnUnits K E).ρ g =
      ((Rep.ofAlgebraAutOnUnits K L).quotientToInvariants
        (AlgEquiv.restrictNormalHom (F := K) (K₁ := L) E).ker).ρ
          ((restrictionQuotientEquiv K L E).symm g) ∘ₗ
        (unitsToKernelInvariantsEquiv K L E).toLinearMap
def

unitsInvariantsRepHom

L125 ↗
ClassFieldTower.Cohomology.unitsInvariantsRepHom
Source context 8 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)
variable [FiniteDimensional K L]
variable [IsGalois K L]
variable [Normal K E]
Lean source · statement
def unitsInvariantsRepHom :
    Rep.res (restrictionQuotientEquiv K L E).toMonoidHom (Rep.ofAlgebraAutOnUnits K E) ⟶
      (Rep.ofAlgebraAutOnUnits K L).quotientToInvariants
        (AlgEquiv.restrictNormalHom (F := K) (K₁ := L) E).ker
def

finiteGaloisUnitsQuotientCohomologyIso

L142 ↗
ClassFieldTower.Cohomology.finiteGaloisUnitsQuotientCohomologyIso
Documentation

Transport from actual lower-field cohomology to quotient-group cohomology with fixed unit coefficients, using restriction and the fixed-field equality.

Source context 8 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)
variable [FiniteDimensional K L]
variable [IsGalois K L]
variable [Normal K E]
Lean source · statement
def finiteGaloisUnitsQuotientCohomologyIso (n : ℕ) :
    groupCohomology (Rep.ofAlgebraAutOnUnits K E) n ≅
      groupCohomology
        ((Rep.ofAlgebraAutOnUnits K L).quotientToInvariants
          (AlgEquiv.restrictNormalHom (F := K) (K₁ := L) E).ker) n
theorem

finiteGaloisUnitsQuotientCohomologyIso_inflation

L152 ↗
ClassFieldTower.Cohomology.finiteGaloisUnitsQuotientCohomologyIso_inflation
Documentation

The fixed-coefficient comparison intertwines quotient inflation with the actual field-unit inflation, including its coefficient map.

Source context 8 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)
variable [FiniteDimensional K L]
variable [IsGalois K L]
variable [Normal K E]
Lean source · statement
theorem finiteGaloisUnitsQuotientCohomologyIso_inflation :
    (finiteGaloisUnitsQuotientCohomologyIso K L E 2).hom ≫
      (groupCohomology.infNatTrans ℤ (AlgEquiv.restrictNormalHom (F := K) (K₁ := L) E).ker 2).app
        (Rep.ofAlgebraAutOnUnits K L) = finiteGaloisUnitsH2Inflation K L E
def

finiteGaloisUnitsH2Restriction

L179 ↗
ClassFieldTower.Cohomology.finiteGaloisUnitsH2Restriction
Documentation

Actual restriction to the relative Galois group, with the field units unchanged.

Source context 8 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)
variable [FiniteDimensional K L]
variable [IsGalois K L]
variable [Normal K E]
Lean source · statement
def finiteGaloisUnitsH2Restriction :
    groupCohomology (Rep.ofAlgebraAutOnUnits K L) 2 ⟶
      groupCohomology (Rep.ofAlgebraAutOnUnits E L) 2
theorem

finiteGaloisUnitsH2Restriction_ker_le_inflation_range

L189 ↗
ClassFieldTower.Cohomology.finiteGaloisUnitsH2Restriction_ker_le_inflation_range
Documentation

Middle exactness for actual field-unit H² in a finite Galois tower. Hilbert 90 supplies the subgroup H¹ vanishing; the quotient comparison identifies the constructed class with lower-field cohomology.

Source context 8 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)
variable [FiniteDimensional K L]
variable [IsGalois K L]
variable [Normal K E]
Lean source · statement
theorem finiteGaloisUnitsH2Restriction_ker_le_inflation_range :
    (finiteGaloisUnitsH2Restriction K L E).hom.ker ≤
      (finiteGaloisUnitsH2Inflation K L E).hom.range

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