Commit 2024-11-11 10:49 73b10f80

View on Github →

refactor(AlgebraicGeometry): weaken RingHom.PropertyIsLocal (#18717)

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

added theorem AlgebraicGeometry.IsAffineOpen.Spec_basicOpen

added theorem AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj

added theorem AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_map

added theorem AlgebraicGeometry.Scheme.Opens.toSpecΓ_top

added def AlgebraicGeometry.SpecMapRestrictBasicOpenIso

Modified Mathlib/AlgebraicGeometry/Cover/Open.lean

added def AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop

Modified Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

added theorem AlgebraicGeometry.stalkwise_Spec_map_iff

added theorem AlgebraicGeometry.stalkwise_isLocalAtSource_of_respectsIso

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

modified theorem AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE

modified theorem AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE_locally

added theorem AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty_of_isLocalAtSource_of_isLocalAtTarget

modified theorem AlgebraicGeometry.HasRingHomProperty.locally_of_iff

added theorem AlgebraicGeometry.HasRingHomProperty.of_isLocalAtSource_of_isLocalAtTarget

added theorem AlgebraicGeometry.HasRingHomProperty.respects_isOpenImmersion

added theorem AlgebraicGeometry.HasRingHomProperty.stalkwise

Modified Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean

Modified Mathlib/RingTheory/LocalProperties/Basic.lean

added theorem RingHom.LocalizationAwayPreserves.respectsIso

added def RingHom.LocalizationAwayPreserves

modified theorem RingHom.LocalizationPreserves.away

added theorem RingHom.OfLocalizationSpanTarget.ofLocalizationSpan

deleted theorem RingHom.PropertyIsLocal.ofLocalizationSpan

added def RingHom.StableUnderCompositionWithLocalizationAwaySource

added def RingHom.StableUnderCompositionWithLocalizationAwayTarget

Modified Mathlib/RingTheory/RingHom/Finite.lean

Modified Mathlib/RingTheory/RingHom/FinitePresentation.lean

Modified Mathlib/RingTheory/RingHom/FiniteType.lean

Modified Mathlib/RingTheory/RingHom/Locally.lean

added theorem RingHom.locally_StableUnderCompositionWithLocalizationAwaySource

added theorem RingHom.locally_StableUnderCompositionWithLocalizationAwayTarget

added theorem RingHom.locally_localizationAwayPreserves

modified theorem RingHom.locally_localizationPreserves

modified theorem RingHom.locally_propertyIsLocal

deleted theorem RingHom.locally_stableUnderCompositionWithLocalizationAway

Modified Mathlib/RingTheory/RingHom/StandardSmooth.lean