Commit 2024-09-24 15:04 b479ce63

View on Github →

chore(Mathlib/RingTheory/LocalProperties): split LocalProperties.lean (#16879) Split the section on local properties in general and the properties that satisfy local properties in LocalProperties.lean into separate files. See the discussions here.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

Modified Mathlib/AlgebraicGeometry/Properties.lean

Modified Mathlib/RingTheory/Ideal/Norm.lean

Modified Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean

Modified Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean

deleted theorem IsIntegrallyClosed.of_localization_maximal

Deleted Mathlib/RingTheory/LocalProperties.lean

deleted theorem Ideal.eq_of_localization_maximal

deleted theorem Ideal.le_of_localization_maximal

deleted theorem IsLocalization.exists_smul_mem_of_mem_adjoin

deleted theorem IsLocalization.lift_mem_adjoin_finsetIntegerMultiple

deleted theorem IsLocalization.smul_mem_finsetIntegerMultiple_span

deleted def LocalizationPreserves

deleted theorem Module.Finite_of_isLocalization

deleted def OfLocalizationMaximal

deleted def RingHom.ContainsIdentities

deleted theorem RingHom.HoldsForLocalizationAway.containsIdentities

deleted theorem RingHom.HoldsForLocalizationAway.of_bijective

deleted def RingHom.HoldsForLocalizationAway

deleted theorem RingHom.LocalizationPreserves.away

deleted def RingHom.LocalizationPreserves

deleted def RingHom.OfLocalizationFiniteSpan

deleted def RingHom.OfLocalizationFiniteSpanTarget

deleted def RingHom.OfLocalizationPrime

deleted def RingHom.OfLocalizationSpan

deleted theorem RingHom.OfLocalizationSpanTarget.ofIsLocalization

deleted def RingHom.OfLocalizationSpanTarget

deleted theorem RingHom.PropertyIsLocal.HoldsForLocalizationAway

deleted theorem RingHom.PropertyIsLocal.ofLocalizationSpan

deleted theorem RingHom.PropertyIsLocal.respectsIso

deleted structure RingHom.PropertyIsLocal

deleted theorem RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway

deleted def RingHom.StableUnderCompositionWithLocalizationAway

deleted theorem RingHom.ofLocalizationSpanTarget_iff_finite

deleted theorem RingHom.ofLocalizationSpan_iff_finite

deleted theorem eq_zero_of_localization

deleted theorem finiteType_ofLocalizationSpan

deleted theorem finite_ofLocalizationSpan

deleted theorem ideal_eq_bot_of_localization'

deleted theorem ideal_eq_bot_of_localization

deleted theorem isIntegrallyClosed_ofLocalizationMaximal

deleted theorem isReduced_ofLocalizationMaximal

deleted theorem localizationPreserves_surjective

deleted theorem localization_away_map_finite

deleted theorem localization_away_map_finiteType

deleted theorem localization_finite

deleted theorem localization_finiteType

deleted theorem localization_isReduced

deleted theorem multiple_mem_adjoin_of_mem_localization_adjoin

deleted theorem multiple_mem_span_of_mem_localization_span

deleted theorem surjective_localRingHom_of_surjective

deleted theorem surjective_ofLocalizationSpan

deleted theorem surjective_respectsIso

Created Mathlib/RingTheory/LocalProperties/Basic.lean

added theorem Ideal.eq_of_localization_maximal

added theorem Ideal.le_of_localization_maximal

added def LocalizationPreserves

added def OfLocalizationMaximal

added def RingHom.ContainsIdentities

added theorem RingHom.HoldsForLocalizationAway.containsIdentities

added theorem RingHom.HoldsForLocalizationAway.of_bijective

added def RingHom.HoldsForLocalizationAway

added theorem RingHom.LocalizationPreserves.away

added def RingHom.LocalizationPreserves

added def RingHom.OfLocalizationFiniteSpan

added def RingHom.OfLocalizationFiniteSpanTarget

added def RingHom.OfLocalizationPrime

added def RingHom.OfLocalizationSpan

added theorem RingHom.OfLocalizationSpanTarget.ofIsLocalization

added def RingHom.OfLocalizationSpanTarget

added theorem RingHom.PropertyIsLocal.HoldsForLocalizationAway

added theorem RingHom.PropertyIsLocal.ofLocalizationSpan

added theorem RingHom.PropertyIsLocal.respectsIso

added structure RingHom.PropertyIsLocal

added theorem RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway

added def RingHom.StableUnderCompositionWithLocalizationAway

added theorem RingHom.ofLocalizationSpanTarget_iff_finite

added theorem RingHom.ofLocalizationSpan_iff_finite

added theorem eq_zero_of_localization

added theorem ideal_eq_bot_of_localization'

added theorem ideal_eq_bot_of_localization

Created Mathlib/RingTheory/LocalProperties/IntegrallyClosed.lean

added theorem IsIntegrallyClosed.of_localization_maximal

added theorem isIntegrallyClosed_ofLocalizationMaximal

Created Mathlib/RingTheory/LocalProperties/Reduced.lean

added theorem isReduced_localizationPreserves

added theorem isReduced_ofLocalizationMaximal

Modified Mathlib/RingTheory/Localization/Finiteness.lean

Modified Mathlib/RingTheory/RingHom/Finite.lean

added theorem IsLocalization.smul_mem_finsetIntegerMultiple_span

added theorem Module.Finite_of_isLocalization

added theorem RingHom.finite_localizationPreserves

added theorem RingHom.finite_ofLocalizationSpan

added theorem RingHom.localization_away_map_finite

added theorem multiple_mem_adjoin_of_mem_localization_adjoin

added theorem multiple_mem_span_of_mem_localization_span

Modified Mathlib/RingTheory/RingHom/FiniteType.lean

added theorem RingHom.IsLocalization.exists_smul_mem_of_mem_adjoin

added theorem RingHom.IsLocalization.lift_mem_adjoin_finsetIntegerMultiple

added theorem RingHom.finiteType_localizationPreserves

added theorem RingHom.finiteType_ofLocalizationSpan

added theorem RingHom.localization_away_map_finiteType

Modified Mathlib/RingTheory/RingHom/Surjective.lean

added theorem RingHom.surjective_localRingHom_of_surjective

added theorem RingHom.surjective_localizationPreserves