Commit 2024-11-06 16:11 3ebc312b

View on Github →

refactor(CategoryTheory/MorphismProperty): turn StableUnderBaseChange into a class (#18692) This allows for less tedious extra arguments.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/Affine.lean

added theorem AlgebraicGeometry.isAffineHom_isStableUnderBaseChange

deleted theorem AlgebraicGeometry.isAffineHom_stableUnderBaseChange

Modified Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean

added theorem AlgebraicGeometry.HasAffineProperty.affineAnd_isStableUnderBaseChange

deleted theorem AlgebraicGeometry.HasAffineProperty.affineAnd_stableUnderBaseChange

added theorem AlgebraicGeometry.affineAnd_isStableUnderBaseChange

deleted theorem AlgebraicGeometry.affineAnd_stableUnderBaseChange

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsStableUnderBaseChange.mk

added def AlgebraicGeometry.AffineTargetMorphismProperty.IsStableUnderBaseChange

deleted theorem AlgebraicGeometry.AffineTargetMorphismProperty.StableUnderBaseChange.mk

deleted def AlgebraicGeometry.AffineTargetMorphismProperty.StableUnderBaseChange

added theorem AlgebraicGeometry.HasAffineProperty.isStableUnderBaseChange

deleted theorem AlgebraicGeometry.HasAffineProperty.stableUnderBaseChange

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

deleted theorem AlgebraicGeometry.IsClosedImmersion.stableUnderBaseChange

Modified Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.isStableUnderBaseChange_of_isStableUnderBaseChangeOnAffine_of_isLocalAtTarget

deleted theorem AlgebraicGeometry.AffineTargetMorphismProperty.stableUnderBaseChange_of_stableUnderBaseChangeOnAffine_of_isLocalAtTarget

Modified Mathlib/AlgebraicGeometry/Morphisms/FinitePresentation.lean

added theorem AlgebraicGeometry.locallyOfFinitePresentation_isStableUnderBaseChange

deleted theorem AlgebraicGeometry.locallyOfFinitePresentation_stableUnderBaseChange

Modified Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean

deleted theorem AlgebraicGeometry.locallyOfFiniteType_stableUnderBaseChange

Modified Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean

deleted theorem AlgebraicGeometry.IsImmersion.stableUnderBaseChange

Modified Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean

deleted theorem AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange

Modified Mathlib/AlgebraicGeometry/Morphisms/Proper.lean

deleted theorem AlgebraicGeometry.IsProper.stableUnderBaseChange

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

deleted theorem AlgebraicGeometry.quasiCompact_stableUnderBaseChange

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

deleted theorem AlgebraicGeometry.quasiSeparated_stableUnderBaseChange

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

added theorem AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange

deleted theorem AlgebraicGeometry.HasRingHomProperty.stableUnderBaseChange

added theorem RingHom.IsStableUnderBaseChange.pullback_fst_app_top

deleted theorem RingHom.StableUnderBaseChange.pullback_fst_app_top

Modified Mathlib/AlgebraicGeometry/Morphisms/Separated.lean

deleted theorem AlgebraicGeometry.IsSeparated.stableUnderBaseChange

Modified Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean

added theorem AlgebraicGeometry.isSmoothOfRelativeDimension_isStableUnderBaseChange

deleted theorem AlgebraicGeometry.isSmoothOfRelativeDimension_stableUnderBaseChange

added theorem AlgebraicGeometry.isSmooth_isStableUnderBaseChange

deleted theorem AlgebraicGeometry.isSmooth_stableUnderBaseChange

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean

deleted theorem AlgebraicGeometry.universallyClosed_stableUnderBaseChange

Modified Mathlib/CategoryTheory/Limits/MorphismProperty.lean

modified theorem CategoryTheory.MorphismProperty.Over.hasPullbacks

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Square.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

added theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.mk'

added theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.universally_eq

added theorem CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.mk'

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.baseChange_map

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.baseChange_obj

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.diagonal

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.fst

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.inf

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.mk

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.monomorphisms

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.op

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.pullback_map

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.respectsIso

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.snd

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.universally_eq

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.unop

deleted def CategoryTheory.MorphismProperty.StableUnderBaseChange

deleted theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.epimorphisms

deleted theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.inf

deleted theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.inl

deleted theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.inr

deleted theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.mk

deleted theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.op

deleted theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.respectsIso

deleted theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.unop

deleted def CategoryTheory.MorphismProperty.StableUnderCobaseChange

added theorem CategoryTheory.MorphismProperty.baseChange_map

added theorem CategoryTheory.MorphismProperty.baseChange_obj

deleted theorem CategoryTheory.MorphismProperty.diagonal_isStableUnderComposition

added theorem CategoryTheory.MorphismProperty.of_isPullback

added theorem CategoryTheory.MorphismProperty.of_isPushout

added theorem CategoryTheory.MorphismProperty.pullback_fst

added theorem CategoryTheory.MorphismProperty.pullback_map

added theorem CategoryTheory.MorphismProperty.pullback_snd

added theorem CategoryTheory.MorphismProperty.pushout_inl

added theorem CategoryTheory.MorphismProperty.pushout_inr

deleted theorem CategoryTheory.MorphismProperty.universally_stableUnderBaseChange

Modified Mathlib/CategoryTheory/MorphismProperty/Representable.lean

deleted theorem CategoryTheory.Functor.relativelyRepresentable.stableUnderBaseChange

added theorem CategoryTheory.MorphismProperty.relative_isStableUnderBaseChange

modified theorem CategoryTheory.MorphismProperty.relative_map

deleted theorem CategoryTheory.MorphismProperty.relative_stableUnderBaseChange

Modified Mathlib/CategoryTheory/Sites/MorphismProperty.lean

modified def CategoryTheory.MorphismProperty.pretopology

modified theorem CategoryTheory.MorphismProperty.pretopology_le

Modified Mathlib/RingTheory/LocalProperties/Basic.lean

added theorem RingHom.IsStableUnderBaseChange.isLocalization_map

added theorem RingHom.IsStableUnderBaseChange.localizationPreserves

added theorem RingHom.IsStableUnderBaseChange.of_isLocalization

deleted theorem RingHom.StableUnderBaseChange.isLocalization_map

deleted theorem RingHom.StableUnderBaseChange.localizationPreserves

deleted theorem RingHom.StableUnderBaseChange.of_isLocalization

Modified Mathlib/RingTheory/RingHom/Finite.lean

added theorem RingHom.finite_isStableUnderBaseChange

deleted theorem RingHom.finite_stableUnderBaseChange

Modified Mathlib/RingTheory/RingHom/FinitePresentation.lean

added theorem RingHom.finitePresentation_isStableUnderBaseChange

deleted theorem RingHom.finitePresentation_stableUnderBaseChange

Modified Mathlib/RingTheory/RingHom/FiniteType.lean

added theorem RingHom.finiteType_isStableUnderBaseChange

deleted theorem RingHom.finiteType_stableUnderBaseChange

Modified Mathlib/RingTheory/RingHom/Integral.lean

added theorem RingHom.isIntegral_isStableUnderBaseChange

deleted theorem RingHom.isIntegral_stableUnderBaseChange

Modified Mathlib/RingTheory/RingHom/Locally.lean

added theorem RingHom.locally_isStableUnderBaseChange

deleted theorem RingHom.locally_stableUnderBaseChange

Modified Mathlib/RingTheory/RingHom/StandardSmooth.lean

added theorem RingHom.isStandardSmoothOfRelativeDimension_isStableUnderBaseChange

deleted theorem RingHom.isStandardSmoothOfRelativeDimension_stableUnderBaseChange

added theorem RingHom.isStandardSmooth_isStableUnderBaseChange

deleted theorem RingHom.isStandardSmooth_stableUnderBaseChange

Modified Mathlib/RingTheory/RingHom/Surjective.lean

added theorem RingHom.surjective_isStableUnderBaseChange

deleted theorem RingHom.surjective_stableUnderBaseChange

Modified Mathlib/RingTheory/RingHomProperties.lean

added theorem RingHom.IsStableUnderBaseChange.mk

added theorem RingHom.IsStableUnderBaseChange.pushout_inl

added def RingHom.IsStableUnderBaseChange

deleted theorem RingHom.StableUnderBaseChange.mk

deleted theorem RingHom.StableUnderBaseChange.pushout_inl

deleted def RingHom.StableUnderBaseChange