English
The forgetful functor forgetToSheafedSpace from LocallyRingedSpace is faithful; equality of morphisms is detected by their underlying SheafedSpace morphisms.
Русский
Функтор забывания forgetToSheafedSpace из LocallyRingedSpace верен; равенство гомоморфизмов определяется по их основанию в SheafedSpace.
LaTeX
$$$ \\text{forgetToSheafedSpace}.Faithful$$
Lean4
instance : forgetToSheafedSpace.ReflectsIsomorphisms where
reflects {_ _} f
i :=
{
out :=
⟨homOfSheafedSpaceHomOfIsIso (CategoryTheory.inv (forgetToSheafedSpace.map f)),
Hom.ext' (IsIso.hom_inv_id (I := i)), Hom.ext' (IsIso.inv_hom_id (I := i))⟩ }
