ClassFieldTower.Martinet.Shafarevich.localSeparableValuationSubring_comap_semilinear
Valuation-compatible base and closure equivalences preserve the selected valuation subrings used to define local residue degree.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open LocalClassFieldTheory LocalFieldTheoryLean source · statement
theorem localSeparableValuationSubring_comap_semilinear
(K K' : Type)
[Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
[Field K'] [ValuativeRel K'] [TopologicalSpace K'] [IsNonarchimedeanLocalField K']
(c : K ≃+* K') (e : SeparableClosure K ≃+* SeparableClosure K')
(he : ∀ x : K, e (algebraMap K (SeparableClosure K) x) =
algebraMap K' (SeparableClosure K') (c x))
(hc : SemilinearValuationCompatible K K' c) :
localSeparableValuationSubring K =
(localSeparableValuationSubring K').comap e.toRingHom