Theorems · Theorem · general topology

CommRingCat.HomTopology.isClosedEmbedding_precomp_of_surjective

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

Hom(A/I, R) is a closed subspace of Hom(A, R) if R is T1.

Defined in

Mathlib.Algebra.Category.Ring.Topology

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceT1Space