Module

FiniteUnramifiedEquiv.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.FiniteUnramifiedEquiv

3 declarations indexed from sourceView source ↗

Module documentation

Unramifiedness across an actual finite local-field equivalence

Integrality produces the integer-ring equivalence from the field equivalence. Transport of the actual maximal-ideal equality then preserves ramification index one. No valuation-preservation certificate is assumed: integral-closure membership supplies it. The two extension towers are fixed explicitly, with no new data instances and one local formally-unramified proof instance.

Imports3

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.FiniteUnramified
Mathlib.RingTheory.RamificationInertia.Ramification
Mathlib.RingTheory.LocalRing.RingHom.Basic

Imported by2

theorem

finiteLocalAlgEquiv_mem_integerRing

L32 ↗

ClassFieldTower.Martinet.Shafarevich.finiteLocalAlgEquiv_mem_integerRing

Source context 6 commands

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

open scoped ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K L M : Type) [Field K] [ValuativeRel K]
  [Field L] [ValuativeRel L] [Field M] [ValuativeRel M]
  [Algebra K L] [Algebra K M]
  [IsIntegralClosure 𝒪[L] 𝒪[K] L] [IsIntegralClosure 𝒪[M] 𝒪[K] M]

Lean source · statement

theorem finiteLocalAlgEquiv_mem_integerRing (e : L ≃ₐ[K] M) (x : 𝒪[L]) :
    e (x : L) ∈ 𝒪[M]

def

finiteLocalIntegerAlgEquiv

L46 ↗

ClassFieldTower.Martinet.Shafarevich.finiteLocalIntegerAlgEquiv

Documentation

Restriction of a field equivalence to the actual integral closures.

Source context 7 commands

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

open scoped ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K L M : Type) [Field K] [ValuativeRel K]
  [Field L] [ValuativeRel L] [Field M] [ValuativeRel M]
  [Algebra K L] [Algebra K M]
  [IsIntegralClosure 𝒪[L] 𝒪[K] L] [IsIntegralClosure 𝒪[M] 𝒪[K] M]
variable
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation M)]

Lean source · full declaration

def finiteLocalIntegerAlgEquiv (e : L ≃ₐ[K] M) : 𝒪[L] ≃ₐ[𝒪[K]] 𝒪[M] where
  toFun x := ⟨e (x : L), finiteLocalAlgEquiv_mem_integerRing K L M e x⟩
  invFun x := ⟨e.symm (x : M), finiteLocalAlgEquiv_mem_integerRing K M L e.symm x⟩
  left_inv x := Subtype.ext (e.symm_apply_apply x)
  right_inv x := Subtype.ext (e.apply_symm_apply x)
  map_mul' x y := Subtype.ext (e.map_mul x y)
  map_add' x y := Subtype.ext (e.map_add x y)
  commutes' x := Subtype.ext (e.commutes (x : K))

theorem

isUnramifiedValuedExtension_of_algEquiv

L62 ↗

ClassFieldTower.Martinet.Shafarevich.isUnramifiedValuedExtension_of_algEquiv

Documentation

Actual unramifiedness transports under a finite local-field equivalence.

Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K L M : Type) [Field K] [ValuativeRel K]
  [Field L] [ValuativeRel L] [Field M] [ValuativeRel M]
  [Algebra K L] [Algebra K M]
  [IsIntegralClosure 𝒪[L] 𝒪[K] L] [IsIntegralClosure 𝒪[M] 𝒪[K] M]
variable
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation M)]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [TopologicalSpace L] [IsNonarchimedeanLocalField L]
  [TopologicalSpace M] [IsNonarchimedeanLocalField M]
  [FiniteDimensional K L] [FiniteDimensional K M]
  [Module.Finite 𝒪[K] 𝒪[L]] [Module.Finite 𝒪[K] 𝒪[M]]

Lean source · statement

theorem isUnramifiedValuedExtension_of_algEquiv (e : L ≃ₐ[K] M)
    [IsUnramifiedValuedExtension K M] : IsUnramifiedValuedExtension K L

Module documentation

Unramifiedness across an actual finite local-field equivalence

Declarations

finiteLocalAlgEquiv_mem_integerRing

finiteLocalIntegerAlgEquiv

isUnramifiedValuedExtension_of_algEquiv