Commit 2024-07-23 19:33 d9ce431c
View on Github →refactor(AlgebraicGeometry): Introduce HasRingHomProperty. (#14992)
HasRingHomProperty P Q is a type class asserting that P is local at the target and the source,
and for f : Spec B ⟶ Spec A, it is equivalent to the ring hom property Q on Γ(f).
This replace the previous API affineLocally that is both slow and hard to use.
This is then used to refactor LocallyOfFiniteType and to deduplicate code.