NYLL
Module

LocalAbsoluteArtinEmbedding.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.LocalAbsoluteArtinEmbedding
2 declarations indexed from sourceView source ↗

Module documentation

Absolute Artin action on an embedded finite extension

An actual representative of the absolute Artin value acts on every embedded finite abelian extension by its finite Artin automorphism. The representative condition is supplied by the quotient map, not by an Artin-comparison assumption.

Imports2
Imported by3

Declarations

theorem

separableAbsoluteLocalArtinMap_lift_action

L30 ↗
ClassFieldTower.Martinet.Shafarevich.separableAbsoluteLocalArtinMap_lift_action
Documentation

Actual Artin action in the separable-closure model.

Source context 5 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (L : Type) [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
theorem separableAbsoluteLocalArtinMap_lift_action
    (i : L →ₐ[K] SeparableClosure K) (a : Kˣ)
    (sigma : Gal(SeparableClosure K/K))
    (hsigma : (QuotientGroup.mk sigma : localAbsoluteAbelianProfinite K) =
      separableAbsoluteLocalArtinMap K a)
    (z : L) :
    sigma (i z) = i (abelianLocalArtinMonoidHom K L a z)
theorem

absoluteLocalArtinMap_lift_action

L66 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteLocalArtinMap_lift_action
Documentation

Actual Artin action in the algebraic-closure model.

Source context 5 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (L : Type) [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · full declaration
theorem absoluteLocalArtinMap_lift_action
    (i : L →ₐ[K] AlgebraicClosure K) (a : Kˣ)
    (sigma : Gal(AlgebraicClosure K/K))
    (hsigma : (QuotientGroup.mk (show Field.absoluteGaloisGroup K from sigma) :
      Field.absoluteGaloisGroupAbelianization K) =
      absoluteLocalArtinMap K a)
    (z : L) :
    sigma (i z) = i (abelianLocalArtinMonoidHom K L a z) := by
  let j : L →ₐ[K] SeparableClosure K :=
    i.codRestrict (separableClosure K (AlgebraicClosure K)).toSubalgebra fun x ↦
      (Algebra.IsSeparable.isSeparable K x).map i i.injective
  let tau := standardToSeparableAbsoluteGaloisEquiv K sigma
  have htau : (QuotientGroup.mk tau : localAbsoluteAbelianProfinite K) =
      separableAbsoluteLocalArtinMap K a := by
    have h := congrArg (separableToStandardAbsoluteAbelianizationEquiv K).symm hsigma
    rw [separableToStandardAbsoluteAbelianizationEquiv_symm_artinMap] at h
    exact h
  exact congrArg (fun x : SeparableClosure K ↦ (x : AlgebraicClosure K))
    (separableAbsoluteLocalArtinMap_lift_action K L j a tau htau z)

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