English
The forgetful functor from TopCommRingCat to TopCat reflects isomorphisms; that is, if a morphism becomes an isomorphism after applying the forgetful functor to TopCat, then the original morphism was an isomorphism in TopCommRingCat.
Русский
Функтор забывания из TopCommRingCat в TopCat отражает изоморфизмы: если образ мока после забывания является изоморфизмом, то исходный мop является изоморфизмом в TopCommRingCat.
LaTeX
$$$\forall X,Y:\ TopCommRingCat,\forall f:\,X\to Y, \big((\forget₂ TopCommRingCat TopCat)(f)\text{ is an isomorphism in TopCat}\big)\Rightarrow f\text{ is an isomorphism in TopCommRingCat}$$$
Lean4
/-- The forgetful functors to `Type` do not reflect isomorphisms,
but the forgetful functor from `TopCommRingCat` to `TopCat` does.
-/
instance : (forget₂ TopCommRingCat.{u} TopCat.{u}).ReflectsIsomorphisms where
reflects {X Y} f
_ := by
-- We have an isomorphism in `TopCat`,
let i_Top :=
asIso
((forget₂ TopCommRingCat TopCat).map f)
-- and a `RingEquiv`.
let e_Ring : X ≃+* Y :=
{ f.1, ((forget TopCat).mapIso i_Top).toEquiv with }
-- Putting these together we obtain the isomorphism we're after:
exact
⟨⟨⟨e_Ring.symm, i_Top.inv.hom.2⟩,
⟨by
ext x
exact e_Ring.left_inv x, by
ext x
exact e_Ring.right_inv x⟩⟩⟩
