feat(number_theory/function_field): add completion with respect to pl…

…ace at infinity (#12715)







Co-authored-by: Johan Commelin <johan@commelin.net>

src/number_theory/function_field.lean

@@ -7,6 +7,7 @@ import field_theory.ratfunc
 import ring_theory.algebraic
 import ring_theory.dedekind_domain.integral_closure
 import ring_theory.integrally_closed
+import topology.algebra.valued_field
 
 /-!
 # Function fields
@@ -18,8 +19,10 @@ This file defines a function field and the ring of integers corresponding to it.
    i.e. it is a finite extension of the field of rational functions in one variable over `Fq`.
  - `function_field.ring_of_integers` defines the ring of integers corresponding to a function field
     as the integral closure of `polynomial Fq` in the function field.
- - `infty_valuation` : The place at infinity on `Fq(t)` is the nonarchimedean valuation on `Fq(t)`
-    with uniformizer `1/t`.
+ - `function_field.infty_valuation` : The place at infinity on `Fq(t)` is the nonarchimedean
+    valuation on `Fq(t)` with uniformizer `1/t`.
+ -  `function_field.Fqt_infty` : The completion `Fq((t⁻¹))`  of `Fq(t)` with respect to the
+    valuation at infinity.
 
 ## Implementation notes
 The definitions that involve a field of fractions choose a canonical field of fractions,
@@ -224,6 +227,73 @@ begin
   rw [infty_valuation_def, if_neg hp', ratfunc.int_degree_polynomial]
 end
 
+/-- The valued field `Fq(t)` with the valuation at infinity. -/
+def infty_valued_Fqt : valued (ratfunc Fq) (with_zero (multiplicative ℤ)) :=
+⟨infty_valuation Fq⟩
+
+lemma infty_valued_Fqt.def {x : ratfunc Fq} :
+  @valued.v (ratfunc Fq) _ _ _ (infty_valued_Fqt Fq) (x) = infty_valuation_def Fq x := rfl
+
+namespace infty_valued_Fqt
+
+/-- The topology structure on `Fq(t)` induced by the valuation at infinity. -/
+def topological_space : topological_space (ratfunc Fq) :=
+@valued.topological_space (ratfunc Fq) _ _ _ (infty_valued_Fqt Fq)
+
+lemma topological_division_ring :
+  @topological_division_ring (ratfunc Fq) _ (topological_space Fq) :=
+@valued.topological_division_ring (ratfunc Fq) _ _ _ (infty_valued_Fqt Fq)
+
+/-- The uniform structure on `k(t)` induced by the valuation at infinity. -/
+def uniform_space : uniform_space (ratfunc Fq) :=
+@topological_add_group.to_uniform_space (ratfunc Fq) _ (topological_space Fq) _
+
+lemma uniform_add_group : @uniform_add_group (ratfunc Fq) (uniform_space Fq) _ :=
+@topological_add_group_is_uniform (ratfunc Fq) _ (topological_space Fq) _
+
+lemma completable_top_field : @completable_top_field (ratfunc Fq) _ (uniform_space Fq) :=
+@valued.completable (ratfunc Fq) _ _ _ (infty_valued_Fqt Fq)
+
+lemma separated_space : @separated_space (ratfunc Fq) (uniform_space Fq) :=
+@valued_ring.separated (ratfunc Fq) _ _ _ (infty_valued_Fqt Fq)
+
+end infty_valued_Fqt
+
+open infty_valued_Fqt
+
+/-- The completion `Fq((t⁻¹))`  of `Fq(t)` with respect to the valuation at infinity. -/
+def Fqt_infty := @uniform_space.completion (ratfunc Fq) (uniform_space Fq)
+
+instance : field (Fqt_infty Fq) :=
+@field_completion (ratfunc Fq) _ (uniform_space Fq) (topological_division_ring Fq) _
+  (uniform_add_group Fq)
+
+instance : inhabited (Fqt_infty Fq) := ⟨(0 : Fqt_infty Fq)⟩
+
+/-- The valuation at infinity on `k(t)` extends to a valuation on `Fqt_infty`. -/
+instance valued_Fqt_infty : valued (Fqt_infty Fq) (with_zero (multiplicative ℤ)) :=
+⟨@valued.extension_valuation (ratfunc Fq) _ _ _ (infty_valued_Fqt Fq)⟩
+
+lemma valued_Fqt_infty.def {x : Fqt_infty Fq} :
+  valued.v (x) = @valued.extension (ratfunc Fq) _ _ _ (infty_valued_Fqt Fq) x := rfl
+
+instance Fqt_infty.topologal_space : topological_space (Fqt_infty Fq) :=
+valued.topological_space (with_zero (multiplicative ℤ))
+
+instance Fqt_infty.topological_division_ring : topological_division_ring (Fqt_infty Fq) :=
+valued.topological_division_ring
+
+instance : topological_ring (Fqt_infty Fq) :=
+(Fqt_infty.topological_division_ring Fq).to_topological_ring
+
+instance : topological_add_group (Fqt_infty Fq) := topological_ring.to_topological_add_group
+
+instance Fqt_infty.uniform_space : uniform_space (Fqt_infty Fq) :=
+topological_add_group.to_uniform_space (Fqt_infty Fq)
+
+instance Fqt_infty.uniform_add_group : uniform_add_group (Fqt_infty Fq) :=
+topological_add_group_is_uniform
+
 end infty_valuation
 
 end function_field