ModuleFinitePlaceCompletionValuationCompatibility.lean
Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.FinitePlaceCompletionValuationCompatibility
3 declarations indexed from sourceView source ↗ Module documentation
Valuation compatibility of the two finite-place completion models
The comparison is an isometry; both valuation relations are exactly the norm comparison relation. This supplies the certificate for actual Artin naturality.
Declarations
ClassFieldTower.Martinet.Shafarevich.finitePlaceCompletionCompatibilitySourceValuativeRel
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (RingOfIntegers F))
ClassFieldTower.Martinet.Shafarevich.finitePlaceCompletionCompatibilityTargetValuativeRel
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (RingOfIntegers F))
local instance finitePlaceCompletionCompatibilitySourceValuativeRel :
ValuativeRel (HeightOneSpectrum.adicAbv F v).Completion :=
finitePlaceLocalArtinCompletionValuativeRel v
ClassFieldTower.Martinet.Shafarevich.finitePlaceCompletion_semilinearValuationCompatible
DocumentationThe canonical completion equivalence preserves the actual valuation relation.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (RingOfIntegers F))
local instance finitePlaceCompletionCompatibilitySourceValuativeRel :
ValuativeRel (HeightOneSpectrum.adicAbv F v).Completion :=
finitePlaceLocalArtinCompletionValuativeRel v
local instance finitePlaceCompletionCompatibilityTargetValuativeRel :
ValuativeRel (v.adicCompletion F) :=
finitePlaceAdicCompletionValuativeRel F v