Commit 2026-01-25 15:24 d56a30e0

View on Github →

feat(AlgebraicGeometry): morphisms of finite type induce essentially of finite type stalk maps (#34101)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean

added theorem AlgebraicGeometry.LocallyOfFiniteType.stalkMap

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

modified theorem AlgebraicGeometry.HasRingHomProperty.stalkMap

added theorem AlgebraicGeometry.HasRingHomProperty.stalkMap_of_respectsIso

Modified Mathlib/RingTheory/EssentialFiniteness.lean

added theorem RingHom.essFiniteType_algebraMap

Modified Mathlib/RingTheory/LocalProperties/Basic.lean

added theorem RingHom.HoldsForLocalization.holdsForLocalizationAway

added theorem RingHom.HoldsForLocalization.isLocalizationMap

added theorem RingHom.HoldsForLocalization.localRingHom

added theorem RingHom.HoldsForLocalization.mk

added def RingHom.HoldsForLocalization

Created Mathlib/RingTheory/RingHom/EssFiniteType.lean

added theorem RingHom.EssFiniteType.comp

added theorem RingHom.EssFiniteType.comp_iff

added theorem RingHom.EssFiniteType.holdsForLocalization

added theorem RingHom.EssFiniteType.isStableUnderBaseChange

added theorem RingHom.EssFiniteType.of_comp

added theorem RingHom.EssFiniteType.residueFieldMap

added theorem RingHom.EssFiniteType.respectsIso

added theorem RingHom.EssFiniteType.stableUnderComposition