Commit 2024-10-16 11:05 36c03bdc

refactor(AlgebraicGeometry): Make Scheme.Hom a structure. (#15093) We make LocallyRingedSpace.Hom (resp. Scheme.Hom) into a structure instead of a subtype (resp. type-synonym of the former) to make clearer the abstraction boundaries between them and presheafed spaces, which allow us to remove some erws. Plus, this enables us to write f.base and f.c instead of f.val.base and f.val.c.