Commit 2025-10-31 13:29 bd4da70b

View on Github →

chore(AlgebraicGeometry): remove unnecessary uses of Hom.base (#30957) The locations were found by a linter, that flagged every occurrence of the chain DFunLike.coe, CategoryTheory.ConcreteCategory.hom , AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom , AlgebraicGeometry.Scheme.Hom.toLRSHom' and an explicit .base projection.

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineTransitionLimit.lean

Modified Mathlib/AlgebraicGeometry/Cover/Directed.lean

Modified Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean

Modified Mathlib/AlgebraicGeometry/Cover/Open.lean

Modified Mathlib/AlgebraicGeometry/Cover/Sigma.lean

Modified Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean

modified theorem AlgebraicGeometry.Scheme.Hom.range_subset_ker_support

modified theorem AlgebraicGeometry.Scheme.Hom.support_ker

Modified Mathlib/AlgebraicGeometry/IdealSheaf/Functorial.lean

Modified Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean

modified theorem AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι

modified theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_apply

Modified Mathlib/AlgebraicGeometry/Morphisms/Affine.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

modified theorem AlgebraicGeometry.Scheme.Hom.isClosedEmbedding

Modified Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Descent.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Flat.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean

modified theorem AlgebraicGeometry.Scheme.Hom.isEmbedding

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Separated.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/SurjectiveOnStalks.lean

modified theorem AlgebraicGeometry.SurjectiveOnStalks.mono_of_injective

Modified Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean

modified theorem AlgebraicGeometry.Scheme.Hom.denseRange

modified theorem AlgebraicGeometry.Scheme.Hom.surjective

modified theorem AlgebraicGeometry.range_eq_univ

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean

modified theorem AlgebraicGeometry.Scheme.Hom.isClosedMap

modified theorem AlgebraicGeometry.Scheme.Hom.isProperMap

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyInjective.lean

modified theorem AlgebraicGeometry.Scheme.Hom.injective

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyOpen.lean

modified theorem AlgebraicGeometry.Flat.generalizingMap

modified theorem AlgebraicGeometry.Scheme.Hom.isOpenMap

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Proper.lean

Modified Mathlib/AlgebraicGeometry/QuasiAffine.lean

Modified Mathlib/AlgebraicGeometry/Scheme.lean

Modified Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean

Modified Mathlib/AlgebraicGeometry/Sites/Small.lean