Forgetting topology on topological commutative rings

The forgetful functor to CommRingCat sends a continuous ring homomorphism to its underlying ring homomorphism. The transport lemma records this also when the source and target have been identified by equalities.

@[simp]

theorem TauCeti.TopCommRingCat.forget₂_map {X Y : TopCommRingCat} (g : X.α →+* Y.α) (hg : Continuous ⇑g) : (CategoryTheory.forget₂ TopCommRingCat CommRingCat).map ⟨g, hg⟩ = CommRingCat.ofHom g

Forgetting the topology of a morphism keeps its underlying ring homomorphism.

theorem TauCeti.TopCommRingCat.forget₂_map_eqToHom_comp_comp_eqToHom {X X' Y Y' : TopCommRingCat} (eX : X = X') (g : X'.α →+* Y'.α) (hg : Continuous ⇑g) (eY : Y = Y') : CategoryTheory.CategoryStruct.comp ((CategoryTheory.forget₂ TopCommRingCat CommRingCat).map (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom eX) (CategoryTheory.CategoryStruct.comp ⟨g, hg⟩ (CategoryTheory.eqToHom ⋯)))) ((CategoryTheory.forget₂ TopCommRingCat CommRingCat).map (CategoryTheory.eqToHom eY)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.forget₂ TopCommRingCat CommRingCat).map (CategoryTheory.eqToHom eX)) (CommRingCat.ofHom g)

Forgetting topology commutes with equality transports at both endpoints.