Theorems · Theorem · functional analysis

Subalgebra.topologicalClosure_comap_homeomorph

∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u} [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : IsSemitopologicalSemiring A] (s : Subalgebra R A) {B : Type u_2}
  [inst_5 : TopologicalSpace B] [inst_6 : Ring B] [inst_7 : IsSemitopologicalRing B] [inst_8 : Algebra R B]
  (f : B →ₐ[R] A) (f' : B ≃ₜ A),
  ⇑f = ⇑f' → Subalgebra.comap f s.topologicalClosure = (Subalgebra.comap f s).topologicalClosure

This is really a statement about topological algebra isomorphisms, but we don't have those, so we use the clunky approach of talking about an algebra homomorphism, and a separate homeomorphism, along with a witness that as functions they are the same.

Defined in

Mathlib.Topology.Algebra.Algebra

Cited by

1 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringTopologicalSpaceSemiringAlgebraIsSemitopologicalSemiringTopologicalSpaceRingIsSemitopologicalRingAlgebra