import topology.basic
import topology.algebra.ring
import algebra.group_power
import ring_theory.subring
import tactic.ring

import for_mathlib.topological_rings
import for_mathlib.nonarchimedean.adic_topology

/-!
# Power bounded elements

The theory of topologically nilpotent, bounded, and power-bounded
elements and subsets of topological rings.
-/

local attribute [instance] set.pointwise_mul_semiring

open set

variables {R : Type*} [comm_ring R] [topological_space R]

/- Note: the following definitions are made without assuming
any compatibility between the algebraic and topological structure on R.
Of course, in applications one will assume that R is a topological ring. -/

/--An element r of a topological ring is topologically nilpotent if for all neighbourhouds U of 0,
there exists a natural number N such that r^n ∈ U for all n > N.
See [Wedhorn, Def 5.25, p. 36]. -/
def is_topologically_nilpotent (r : R) : Prop :=
∀ U ∈ (nhds (0 : R)), ∃ N : ℕ, ∀ n : ℕ, n > N → r^n ∈ U

/--A subset T of a topological ring is topologically nilpotent if for all neighbourhouds U of 0,
there exists a natural number N such that r^n ∈ U for all n > N.
(Here T^n is the set {t₁ * t₂ * ⋯ * tₙ | t₁, t₂, …, tₙ ∈ T}.) -/
def is_topologically_nilpotent_subset (T : set R) : Prop :=
∀ U ∈ (nhds (0 : R)), ∃ n : ℕ, T ^ n ⊆ U

/--A subset B of a topological ring is bounded if for all neighbourhoods U of 0 ∈ R,
there exists a neighbourhood V or 0 such that for all v ∈ V and b ∈ B we have v*b ∈ U.
See [Wedhorn, Def 5.27, p. 36]. -/
def is_bounded (B : set R) : Prop :=
∀ U ∈ nhds (0 : R), ∃ V ∈ nhds (0 : R), ∀ v ∈ V, ∀ b ∈ B, v*b ∈ U

/--A subset B of a topological ring is bounded if and only if for all neighbourhoods U of 0 ∈ R,
there exists a neighbourhood V or 0 such that for all v ∈ V and b ∈ B we have V*B ⊆ U.
(Here V*B denotes the set {v * b | v ∈ V, b ∈ B}.) -/
lemma is_bounded_iff (B : set R) :
  is_bounded B ↔ ∀ U ∈ nhds (0 : R), ∃ V ∈ nhds (0 : R), V * B ⊆ U :=
forall_congr $ λ U, imp_congr iff.rfl $ exists_congr $ λ V, exists_congr $ λ hV,
begin
  split,
  { rintros H _ ⟨v, hv, b, hb, rfl⟩, exact H v hv b hb },
  { intros H v hv b hb, exact H ⟨v, hv, b, hb, rfl⟩ }
end

section topological_ring
variables [topological_ring R]

/--A topological ring with adic topology is bounded.-/
lemma is_adic.is_bounded (h : is_adic R) : is_bounded (univ : set R) :=
begin
  intros U hU,
  rw mem_nhds_sets_iff at hU,
  rcases hU with ⟨V, hV₁, ⟨hV₂, h0⟩⟩,
  tactic.unfreeze_local_instances,
  rcases h with ⟨J, hJ⟩,
  rw is_ideal_adic_iff at hJ,
  have H : (∃ (n : ℕ), (J^n).carrier ⊆ V) :=
  begin
    apply hJ.2,
    exact mem_nhds_sets hV₂ h0,
  end,
  rcases H with ⟨n, hn⟩,
  use (J^n).carrier, -- the key step
  split,
  { exact mem_nhds_sets (hJ.1 n) (J^n).zero_mem },
  { rintros a ha b hb,
    apply hV₁,
    exact hn ((J^n).mul_mem_right ha), }
end

section
open submodule topological_add_group

set_option class.instance_max_depth 58

/--A subset B of a nonarchimedean ring is bounded if and only if
for all neighbourhoods U of 0 ∈ R, there exists an open additive subgroup V such that
V * B generates a subgroup contained in U. -/
lemma is_bounded_add_subgroup_iff (hR : nonarchimedean R) (B : set R) :
  is_bounded B ↔ ∀ U ∈ nhds (0:R), ∃ V : open_add_subgroup R,
    (↑((V : set R) • span ℤ B) : set R) ⊆ U :=
begin
  split,
  { rintros H U hU,
    cases hR U hU with W hW,
    rw is_bounded_iff at H,
    rcases H _ W.mem_nhds_zero with ⟨V', hV', H'⟩,
    cases hR V' hV' with V hV,
    use V,
    refine set.subset.trans _ hW,
    change ↑(span _ _ * span _ _) ⊆ _,
    rw [span_mul_span, span_int_eq_add_group_closure, add_group.closure_subset_iff],
    exact set.subset.trans (set.pointwise_mul_subset_mul hV (set.subset.refl B)) H' },
  { intros H,
    rw is_bounded_iff,
    intros U hU,
    cases H U hU with V hV,
    use [V, V.mem_nhds_zero],
    refine set.subset.trans _ hV,
    rintros _ ⟨v, hv, b, hb, rfl⟩,
    exact mul_mem_mul (subset_span hv) (subset_span hb) }
end

/--If J is an ideal in a topological ring whose topology is J-adic,
then J is topologically nilpotent.-/
lemma is_ideal_adic.topologically_nilpotent {J : ideal R} (h : is-J-adic) :
  is_topologically_nilpotent_subset (↑J : set R) :=
begin
  rw is_ideal_adic_iff at h,
  intros U hU,
  cases h.2 U hU with n hn,
  use n,
  exact set.subset.trans (J.pow_subset_pow) hn
end

end

end topological_ring

namespace is_bounded
open topological_add_group

/--A subset of a bounded subset is bounded. See [Wedhorn, Rmk 5.28(2)].-/
lemma subset {S₁ S₂ : set R} (h : S₁ ⊆ S₂) (H : is_bounded S₂) : is_bounded S₁ :=
begin
  intros U hU,
  rcases H U hU with ⟨V, hV₁, hV₂⟩,
  use [V, hV₁],
  intros v hv b hb,
  exact hV₂ _ hv _ (h hb),
end

/--The subgroup generated by a bounded subset of a nonarchimedean ring is bounded.
See [Wedhorn, Prop 5.30(1)].-/
lemma add_group.closure [topological_ring R] (hR : nonarchimedean R) (T : set R)
  (hT : is_bounded T) : is_bounded (add_group.closure T) :=
begin
  intros U hU,
  -- find subgroup U' in U
  rcases hR U hU with ⟨U', hU'⟩,
  -- U' still a nhd
  -- Use boundedness hypo for T with U' to get V
  rcases hT (U' : set R) U'.mem_nhds_zero with ⟨V, hV, hB⟩,
  -- find subgroup V' in V
  rcases hR V hV with ⟨V', hV'⟩,
  -- V' works for our proof
  use [V', V'.mem_nhds_zero],
  intros v hv b hb,
  -- Suffices to prove we're in U'
  apply hU',
  -- Prove the result by induction
  apply add_group.in_closure.rec_on hb,
  { intros t ht,
    exact hB v (hV' hv) t ht },
  { rw mul_zero, exact U'.zero_mem },
  { intros a Ha Hv,
    rwa [←neg_mul_comm, neg_mul_eq_neg_mul_symm, is_add_subgroup.neg_mem_iff] },
  { intros a b ha hb Ha Hb,
    rw [mul_add],
    exact U'.add_mem Ha Hb }
end

end is_bounded

/--An element r of a topological ring is power bounded if the set of all positive powers of r
is a bounded subset. See [Wedhorn, Def 5.27].-/
definition is_power_bounded (r : R) : Prop := is_bounded (powers r)

/--A subset T of a topological ring is power bounded if the submonoid generated by T is bounded.
See [Wedhorn, Def 5.27].-/
definition is_power_bounded_subset (T : set R) : Prop := is_bounded (monoid.closure T)

namespace power_bounded
open topological_add_group

/-- 0 is power bounded.-/
lemma zero : is_power_bounded (0 : R) :=
λ U hU, ⟨U,
begin
  split, {exact hU},
  intros v hv b H,
  induction H with n H,
  induction n ; { simp [H.symm, pow_succ, mem_of_nhds hU], try {assumption} }
end⟩

/-- 1 is power bounded.-/
lemma one : is_power_bounded (1 : R) :=
λ U hU, ⟨U,
begin
  split, {exact hU},
  intros v hv b H,
  cases H with n H,
  simpa [H.symm]
end⟩

/-- An element r is power bounded if and only if the singleton {r} is power bounded.-/
lemma singleton (r : R) : is_power_bounded r ↔ is_power_bounded_subset ({r} : set R) :=
begin
  unfold is_power_bounded,
  unfold is_power_bounded_subset,
  rw monoid.closure_singleton,
end

/-- A subset of a power bounded set is power bounded. See [Wedhorn, Rmk 5.28(2)].-/
lemma subset {B C : set R} (h : B ⊆ C) (hC : is_power_bounded_subset C) :
  is_power_bounded_subset B :=
λ U hU, exists.elim (hC U hU) $
  λ V ⟨hV, hC⟩, ⟨V, hV, λ v hv b hb, hC v hv b $ monoid.closure_mono h hb⟩

/--The union of two power bounded sets is power bounded. See [Wedhorn, Rmk 5.28(3)].-/
lemma union {S T : set R} (hS : is_power_bounded_subset S) (hT : is_power_bounded_subset T) :
  is_power_bounded_subset (S ∪ T) :=
begin
  intros U hU,
  rcases hT U hU with ⟨V, hV, hVU⟩,
  rcases hS V hV with ⟨W, hW, hWV⟩,
  use [W, hW],
  intros v hv b hb,
  rw monoid.mem_closure_union_iff at hb,
  rcases hb with ⟨y, hy, z, hz, rfl⟩,
  rw [←mul_assoc],
  apply hVU _ _ _ hz,
  exact hWV _ hv _ hy,
end

/--The monoid generated by a power bounded subset is power bounded.-/
lemma monoid.closure {T : set R}
  (hT : is_power_bounded_subset T) : is_power_bounded_subset (monoid.closure T) :=
begin
  refine is_bounded.subset _ hT,
  apply monoid.closure_subset,
  refl
end

/--The product of two power bounded elements is power bounded.-/
lemma mul (a b : R)
  (ha : is_power_bounded a) (hb : is_power_bounded b) :
  is_power_bounded (a * b) :=
begin
  rw singleton at ha hb ⊢,
  refine subset _ (monoid.closure (union ha hb)),
  rw [set.singleton_subset_iff, monoid.mem_closure_union_iff],
  refine ⟨a, _, b, _, rfl⟩; exact monoid.subset_closure (set.mem_singleton _)
end

section topological_ring
variables [topological_ring R]

/--The subgroup generated by a power bounded subset of a nonarchimedean ring is power bounded.
See [Wedhorn, Prop 5.30(1)].-/
lemma add_group.closure (hR : nonarchimedean R) {T : set R}
  (hT : is_power_bounded_subset T) : is_power_bounded_subset (add_group.closure T) :=
begin
  refine is_bounded.subset _ (is_bounded.add_group.closure hR _ hT),
  intros a ha,
  apply monoid.in_closure.rec_on ha,
  { apply add_group.closure_mono,
    exact monoid.subset_closure },
  { apply add_group.mem_closure,
    exact monoid.in_closure.one _ },
  { intros a b ha hb Ha Hb,
    show a * b ∈ ring.closure T,
    exact is_submonoid.mul_mem Ha Hb }
end

/--The subring generated by a power bounded subset of a nonarchimedean ring is power bounded.
See [Wedhorn, Prop 5.30(2)].-/
lemma ring.closure (hR : nonarchimedean R) (T : set R)
  (hT : is_power_bounded_subset T) : is_power_bounded_subset (ring.closure T) :=
add_group.closure hR $ monoid.closure hT

/--The subring generated by a power bounded subset of a nonarchimedean ring is bounded.-/
lemma ring.closure' (hR : nonarchimedean R) (T : set R)
  (hT : is_power_bounded_subset T) : is_bounded (_root_.ring.closure T) :=
is_bounded.subset monoid.subset_closure (ring.closure hR _ hT)

/--The sum of two power bounded elements of a nonarchimedean ring is power bounded.-/
lemma add (hR : nonarchimedean R) (a b : R)
  (ha : is_power_bounded a) (hb : is_power_bounded b) :
  is_power_bounded (a + b) :=
begin
  rw singleton at ha hb ⊢,
  refine subset _ (add_group.closure hR (union ha hb)),
  rw set.singleton_subset_iff,
  apply is_add_submonoid.add_mem;
    apply add_group.subset_closure; simp
end

end topological_ring

end power_bounded

variable (R)

/-- The subring of power bounded elements.
(Note that this definition makes sense for all R,
but this subset is only a subring for certain rings, such as non-archimedean rings.) -/
definition power_bounded_subring := {r : R | is_power_bounded r}

variable {R}

namespace power_bounded_subring
open topological_add_group

/--The coercion from the power bounded subring to the ambient ring.-/
instance : has_coe (power_bounded_subring R) R := ⟨subtype.val⟩

lemma zero_mem : (0 : R) ∈ power_bounded_subring R := power_bounded.zero

lemma one_mem : (1 : R) ∈ power_bounded_subring R := power_bounded.one

lemma mul_mem :
  ∀ ⦃a b : R⦄, a ∈ power_bounded_subring R → b ∈ power_bounded_subring R →
  a * b ∈ power_bounded_subring R :=
power_bounded.mul

/--The subset of power bounded elements of a topological ring is a submonoid.-/
instance : is_submonoid (power_bounded_subring R) :=
{ one_mem := one_mem,
  mul_mem := mul_mem }

section topological_ring
variables [topological_ring R]

lemma add_mem (h : nonarchimedean R) ⦃a b : R⦄
  (ha : a ∈ power_bounded_subring R) (hb : b ∈ power_bounded_subring R) :
  a + b ∈ power_bounded_subring R :=
power_bounded.add h a b ha hb

lemma neg_mem : ∀ ⦃a : R⦄, a ∈ power_bounded_subring R → -a ∈ power_bounded_subring R :=
λ a ha U hU,
begin
  let Usymm := U ∩ {u | -u ∈ U},
  have hUsymm : Usymm ∈ (nhds (0 : R)) :=
  begin
    apply filter.inter_mem_sets hU,
    apply continuous.tendsto (topological_add_group.continuous_neg R) 0,
    simpa
  end,
  rcases ha Usymm hUsymm with ⟨V, ⟨V_nhd, hV⟩⟩,
  use [V, V_nhd],
  rintros v hv _ ⟨n, rfl⟩,
  rw show v * (-a)^n = ((-1)^n * v) * a^n,
  by { rw [neg_eq_neg_one_mul, mul_pow], ring },
  suffices H : (-1)^n * v * a^n ∈ Usymm,
  { exact H.left },
  have H := hV v hv (a^n) ⟨n, rfl⟩,
  cases (@neg_one_pow_eq_or R _ n) with h h;
    simpa [h, H.1, H.2] using H
end

/--The subset of power bounded elements of a nonarchimedean ring is a subgroup.-/
instance (hR : nonarchimedean R) : is_add_subgroup (power_bounded_subring R) :=
{ zero_mem := zero_mem,
  add_mem := add_mem hR,
  neg_mem := neg_mem  }

/--The subset of power bounded elements of a nonarchimedean ring is a subring.-/
instance (hR : nonarchimedean R) : is_subring (power_bounded_subring R) :=
{ ..power_bounded_subring.is_submonoid,
  ..power_bounded_subring.is_add_subgroup hR }

end topological_ring

variable (R)

/--A topological ring is uniform if the subset of power bounded elements is bounded.-/
definition is_uniform : Prop := is_bounded (power_bounded_subring R)

end power_bounded_subring
