English
A canonical homeomorphism between SeparationQuotient α and α ⧸ closure(⊥) exists for a commutative ring α with topology and topological ring structure.
Русский
Существуют канонические гомеоморфизмы между разделенной фактор-группой и фактор-группой по замыканию нуля для кольца α с топологией.
LaTeX
$$sepQuotHomeomorphRingQuot(α)$$
Lean4
/-- Given a topological ring `α` equipped with a uniform structure that makes subtraction uniformly
continuous, get an homeomorphism between the separated quotient of `α` and the quotient ring
corresponding to the closure of zero. -/
def sepQuotHomeomorphRingQuot (α) [CommRing α] [TopologicalSpace α] [IsTopologicalRing α] :
SeparationQuotient α ≃ₜ α ⧸ (⊥ : Ideal α).closure
where
toEquiv := Quotient.congrRight fun x y => by rw [inseparableSetoid_ring]
continuous_toFun := continuous_id.quotient_map' <| by rw [inseparableSetoid_ring]; exact fun _ _ ↦ id
continuous_invFun := continuous_id.quotient_map' <| by rw [inseparableSetoid_ring]; exact fun _ _ ↦ id
