import topology.algebra.nonarchimedean.bases

import topology.algebra.uniform_filter_basis

import ring_theory.valuation.basic

open_locale classical topology uniformity

open set valuation

noncomputable theory

universes v u

variables {R : Type u} [ring R] {Γ₀ : Type v} [linear_ordered_comm_group_with_zero Γ₀]

namespace valuation

variables (v : valuation R Γ₀)

lemma subgroups_basis :

ring_subgroups_basis (λ γ : Γ₀ˣ, (v.lt_add_subgroup γ : add_subgroup R)) :=

{ inter := begin

rintros γ₀ γ₁,

use min γ₀ γ₁,

simp [valuation.lt_add_subgroup] ; tauto

end,

mul := begin

rintros γ,

cases exists_square_le γ with γ₀ h,

use γ₀,

rintro - ⟨r, s, r_in, s_in, rfl⟩,

calc (v (r*s) : Γ₀) = v r * v s : valuation.map_mul _ _ _

... < γ₀*γ₀ : mul_lt_mul₀ r_in s_in

... ≤ γ : by exact_mod_cast h

end,

left_mul := begin

rintros x γ,

rcases group_with_zero.eq_zero_or_unit (v x) with Hx | ⟨γx, Hx⟩,

{ use (1 : Γ₀ˣ),

rintros y (y_in : (v y : Γ₀) < 1),

change v (x * y) < _,

rw [valuation.map_mul, Hx, zero_mul],

exact units.zero_lt γ },

{ simp only [image_subset_iff, set_of_subset_set_of, preimage_set_of_eq, valuation.map_mul],

use γx⁻¹*γ,

rintros y (vy_lt : v y < ↑(γx⁻¹ * γ)),

change (v (x * y) : Γ₀) < γ,

rw [valuation.map_mul, Hx, mul_comm],

rw [units.coe_mul, mul_comm] at vy_lt,

simpa using mul_inv_lt_of_lt_mul₀ vy_lt }

end,

right_mul := begin

rintros x γ,

rcases group_with_zero.eq_zero_or_unit (v x) with Hx | ⟨γx, Hx⟩,

{ use 1,

rintros y (y_in : (v y : Γ₀) < 1),

change v (y * x) < _,

rw [valuation.map_mul, Hx, mul_zero],

exact units.zero_lt γ },

{ use γx⁻¹*γ,

rintros y (vy_lt : v y < ↑(γx⁻¹ * γ)),

change (v (y * x) : Γ₀) < γ,

rw [valuation.map_mul, Hx],

rw [units.coe_mul, mul_comm] at vy_lt,

simpa using mul_inv_lt_of_lt_mul₀ vy_lt }

end }

end valuation

class valued (R : Type u) [ring R] (Γ₀ : out_param (Type v))

[linear_ordered_comm_group_with_zero Γ₀] extends uniform_space R, uniform_add_group R :=

(v : valuation R Γ₀)

(is_topological_valuation : ∀ s, s ∈ 𝓝 (0 : R) ↔ ∃ (γ : Γ₀ˣ), { x : R | v x < γ } ⊆ s)

attribute [nolint dangerous_instance] valued.to_uniform_space

namespace valued

def mk' (v : valuation R Γ₀) : valued R Γ₀ :=

{ v := v,

to_uniform_space := @topological_add_group.to_uniform_space R _ v.subgroups_basis.topology _,

to_uniform_add_group := @topological_add_comm_group_is_uniform _ _ v.subgroups_basis.topology _,

is_topological_valuation :=

begin

letI := @topological_add_group.to_uniform_space R _ v.subgroups_basis.topology _,

intros s,

rw filter.has_basis_iff.mp v.subgroups_basis.has_basis_nhds_zero s,

exact exists_congr (λ γ, by simpa),

end }

variables (R Γ₀) [_i : valued R Γ₀]

include _i

lemma has_basis_nhds_zero :

(𝓝 (0 : R)).has_basis (λ _, true) (λ (γ : Γ₀ˣ), { x | v x < (γ : Γ₀) }) :=

by simp [filter.has_basis_iff, is_topological_valuation]

lemma has_basis_uniformity :

(𝓤 R).has_basis (λ _, true) (λ (γ : Γ₀ˣ), { p : R × R | v (p.2 - p.1) < (γ : Γ₀) }) :=

rw uniformity_eq_comap_nhds_zero,

exact (has_basis_nhds_zero R Γ₀).comap _,

lemma to_uniform_space_eq :

to_uniform_space = @topological_add_group.to_uniform_space R _ v.subgroups_basis.topology _ :=

uniform_space_eq

((has_basis_uniformity R Γ₀).eq_of_same_basis $ v.subgroups_basis.has_basis_nhds_zero.comap _)

variables {R Γ₀}

lemma mem_nhds {s : set R} {x : R} :

(s ∈ 𝓝 x) ↔ ∃ (γ : Γ₀ˣ), {y | (v (y - x) : Γ₀) < γ } ⊆ s :=

by simp only [← nhds_translation_add_neg x, ← sub_eq_add_neg, preimage_set_of_eq, exists_true_left,

((has_basis_nhds_zero R Γ₀).comap (λ y, y - x)).mem_iff]

lemma mem_nhds_zero {s : set R} :

(s ∈ 𝓝 (0 : R)) ↔ ∃ γ : Γ₀ˣ, {x | v x < (γ : Γ₀) } ⊆ s :=

by simp only [mem_nhds, sub_zero]

lemma loc_const {x : R} (h : (v x : Γ₀) ≠ 0) : {y : R | v y = v x} ∈ 𝓝 x :=

rw mem_nhds,

rcases units.exists_iff_ne_zero.mpr h with ⟨γ, hx⟩,

use γ,

rw hx,

intros y y_in,

exact valuation.map_eq_of_sub_lt _ y_in

instance : topological_ring R :=

(to_uniform_space_eq R Γ₀).symm ▸ v.subgroups_basis.to_ring_filter_basis.is_topological_ring

lemma cauchy_iff {F : filter R} :

cauchy F ↔ F.ne_bot ∧ ∀ γ : Γ₀ˣ, ∃ M ∈ F, ∀ x y ∈ M, (v (y - x) : Γ₀) < γ :=

rw [to_uniform_space_eq, add_group_filter_basis.cauchy_iff],

apply and_congr iff.rfl,

simp_rw valued.v.subgroups_basis.mem_add_group_filter_basis_iff,

split,

{ intros h γ,

exact h _ (valued.v.subgroups_basis.mem_add_group_filter_basis _) },

{ rintros h - ⟨γ, rfl⟩,

exact h γ }

end valued