English
If a ring is equipped with a topology coming from a ring filter basis, then it becomes a topological ring; the multiplication and addition are continuous with respect to that topology and the relevant translations behave well.
Русский
Если кольцо упростить топологией, полученной из фильтр-базы кольца, то оно становится топологическим кольцом; сложение и умножение непрерывны в этой топологии и соответствующие переносы ведут себя совместимо.
LaTeX
$$$(R, BR.topology)$ is a topological ring.$$
Lean4
/-- If a ring is endowed with a topological structure coming from
a ring filter basis then it's a topological ring. -/
instance (priority := 100) isTopologicalRing {R : Type u} [Ring R] (B : RingFilterBasis R) :
@IsTopologicalRing R B.topology _ := by
let B' := B.toAddGroupFilterBasis
letI := B'.topology
have basis := B'.nhds_zero_hasBasis
have basis' := basis.prod basis
haveI := B'.isTopologicalAddGroup
apply IsTopologicalRing.of_addGroup_of_nhds_zero
· rw [basis'.tendsto_iff basis]
suffices ∀ U ∈ B', ∃ V W, (V ∈ B' ∧ W ∈ B') ∧ ∀ a b, a ∈ V → b ∈ W → a * b ∈ U by simpa
intro U U_in
rcases B.mul U_in with ⟨V, V_in, hV⟩
refine ⟨V, V, ⟨V_in, V_in⟩, ?_⟩
intro a b a_in b_in
exact hV <| mul_mem_mul a_in b_in
· intro x₀
rw [basis.tendsto_iff basis]
intro U
simpa using B.mul_left x₀
· intro x₀
rw [basis.tendsto_iff basis]
intro U
simpa using B.mul_right x₀
