Theorems · Theorem · general topology

CommRingCat.HomTopology.isEmbedding_precomp_of_surjective

∀ {R A B : CommRingCat} [inst : TopologicalSpace ↑R] (f : A ⟶ B),
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f) →
    Topology.IsEmbedding fun x => CategoryTheory.CategoryStruct.comp f x

Hom(A/I, R) has the subspace topology of Hom(A, R). More generally, a surjection A ⟶ B gives rise to an embedding Hom(B, R) ⟶ Hom(A, R)

Defined in

Mathlib.Algebra.Category.Ring.Topology

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpace