LocalFieldTheory.isValuativeTopology_of_valued_ofValuation
The topology of a nontrivially valued field is valuative for the valuative relation induced by its distinguished valuation.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalFieldTheory
open scoped ValuativeRel
universe u vLean source · full declaration
theorem isValuativeTopology_of_valued_ofValuation
(F : Type u) (Γ : Type v)
[Field F] [LinearOrderedCommGroupWithZero Γ]
[MulArchimedean Γ] [Valued F Γ]
[Valuation.IsNontrivial (Valued.v : Valuation F Γ)] :
letI := ValuativeRel.ofValuation (Valued.v : Valuation F Γ)
IsValuativeTopology F := by
let v : Valuation F Γ := Valued.v
let : ValuativeRel F := ValuativeRel.ofValuation v
let : v.Compatible := Valuation.Compatible.ofValuation v
let : ValuativeRel.IsNontrivial F :=
(ValuativeRel.isNontrivial_iff_isNontrivial v).2 inferInstance
apply IsValuativeTopology.of_zero
intro s
rw [Valued.mem_nhds_zero]
constructor
· rintro ⟨δ, hδ⟩
refine
⟨δ.mapEquiv
(ValuativeRel.ValueGroupWithZero.orderMonoidIso v).symm, ?_⟩
intro z hz
apply hδ
exact
(ValuativeRel.valuation_lt_symm_orderMonoidIso
v δ.1 z).1
(by simpa using hz)
· rintro ⟨γ, hγ⟩
refine
⟨γ.mapEquiv
(ValuativeRel.ValueGroupWithZero.orderMonoidIso v), ?_⟩
intro z hz
apply hγ
have hz' :
v.restrict z <
(ValuativeRel.ValueGroupWithZero.orderMonoidIso v)
γ.1 := by
exact hz
exact
(ValuativeRel.restrict_lt_orderMonoidIso
v γ.1 z).1 hz'