Commit 2025-02-07 16:33 97ed5e0a

View on Github →

chore(RingTheory/Ideal/Over): factor going-up results out (#21497) Also move Ideal.comap_map_eq_self_iff_of_isPrime to Mathlib.RingTheory.Localization.AtPrime.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/DedekindDomain/Basic.lean

Created Mathlib/RingTheory/Ideal/GoingUp.lean

added theorem Ideal.IntegralClosure.comap_lt_comap

added theorem Ideal.IntegralClosure.comap_ne_bot

added theorem Ideal.IntegralClosure.eq_bot_of_comap_eq_bot

added theorem Ideal.IntegralClosure.isMaximal_of_isMaximal_comap

added theorem Ideal.IsIntegralClosure.comap_lt_comap

added theorem Ideal.IsIntegralClosure.comap_ne_bot

added theorem Ideal.IsIntegralClosure.eq_bot_of_comap_eq_bot

added theorem Ideal.IsIntegralClosure.isMaximal_of_isMaximal_comap

added theorem Ideal.IsMaximal.of_isMaximal_liesOver

added theorem Ideal.IsMaximal.of_liesOver_isMaximal

added theorem Ideal.coeff_zero_mem_comap_of_root_mem

added theorem Ideal.coeff_zero_mem_comap_of_root_mem_of_eval_mem

added theorem Ideal.comap_lt_comap_of_integral_mem_sdiff

added theorem Ideal.comap_lt_comap_of_root_mem_sdiff

added theorem Ideal.comap_ne_bot_of_algebraic_mem

added theorem Ideal.comap_ne_bot_of_integral_mem

added theorem Ideal.comap_ne_bot_of_root_mem

added theorem Ideal.eq_bot_of_comap_eq_bot

added theorem Ideal.exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff

added theorem Ideal.exists_coeff_ne_zero_mem_comap_of_non_zero_divisor_root_mem

added theorem Ideal.exists_coeff_ne_zero_mem_comap_of_root_mem

added theorem Ideal.exists_ideal_comap_le_prime

added theorem Ideal.exists_ideal_liesOver_maximal_of_isIntegral

added theorem Ideal.exists_ideal_over_maximal_of_isIntegral

added theorem Ideal.exists_ideal_over_prime_of_isIntegral

added theorem Ideal.exists_ideal_over_prime_of_isIntegral_of_isDomain

added theorem Ideal.exists_ideal_over_prime_of_isIntegral_of_isPrime

added theorem Ideal.exists_nonzero_mem_of_ne_bot

added theorem Ideal.injective_quotient_le_comap_map

added theorem Ideal.isMaximal_comap_of_isIntegral_of_isMaximal'

added theorem Ideal.isMaximal_comap_of_isIntegral_of_isMaximal

added theorem Ideal.isMaximal_of_isIntegral_of_isMaximal_comap'

added theorem Ideal.isMaximal_of_isIntegral_of_isMaximal_comap

added theorem Ideal.map_eq_top_iff

added theorem Ideal.map_eq_top_iff_of_ker_le

added theorem Ideal.mem_of_one_mem

added theorem Ideal.primesOver_bot

added theorem Ideal.quotient_mk_maps_eq

Modified Mathlib/RingTheory/Ideal/Maps.lean

added theorem Ideal.comap_map_eq_self_iff_of_isPrime

added theorem Ideal.disjoint_map_primeCompl_iff_comap_le

Modified Mathlib/RingTheory/Ideal/Operations.lean

added theorem Ideal.primeCompl_le_nonZeroDivisors

Modified Mathlib/RingTheory/Ideal/Over.lean

deleted theorem Ideal.IntegralClosure.comap_lt_comap

deleted theorem Ideal.IntegralClosure.comap_ne_bot

deleted theorem Ideal.IntegralClosure.eq_bot_of_comap_eq_bot

deleted theorem Ideal.IntegralClosure.isMaximal_of_isMaximal_comap

deleted theorem Ideal.IsIntegralClosure.comap_lt_comap

deleted theorem Ideal.IsIntegralClosure.comap_ne_bot

deleted theorem Ideal.IsIntegralClosure.eq_bot_of_comap_eq_bot

deleted theorem Ideal.IsIntegralClosure.isMaximal_of_isMaximal_comap

deleted theorem Ideal.IsMaximal.of_isMaximal_liesOver

deleted theorem Ideal.IsMaximal.of_liesOver_isMaximal

deleted theorem Ideal.coeff_zero_mem_comap_of_root_mem

deleted theorem Ideal.coeff_zero_mem_comap_of_root_mem_of_eval_mem

deleted theorem Ideal.comap_lt_comap_of_integral_mem_sdiff

deleted theorem Ideal.comap_lt_comap_of_root_mem_sdiff

deleted theorem Ideal.comap_map_eq_self_iff_of_isPrime

deleted theorem Ideal.comap_ne_bot_of_algebraic_mem

deleted theorem Ideal.comap_ne_bot_of_integral_mem

deleted theorem Ideal.comap_ne_bot_of_root_mem

deleted theorem Ideal.eq_bot_of_comap_eq_bot

deleted theorem Ideal.exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff

deleted theorem Ideal.exists_coeff_ne_zero_mem_comap_of_non_zero_divisor_root_mem

deleted theorem Ideal.exists_coeff_ne_zero_mem_comap_of_root_mem

deleted theorem Ideal.exists_ideal_comap_le_prime

deleted theorem Ideal.exists_ideal_liesOver_maximal_of_isIntegral

deleted theorem Ideal.exists_ideal_over_maximal_of_isIntegral

deleted theorem Ideal.exists_ideal_over_prime_of_isIntegral

deleted theorem Ideal.exists_ideal_over_prime_of_isIntegral_of_isDomain

deleted theorem Ideal.exists_ideal_over_prime_of_isIntegral_of_isPrime

deleted theorem Ideal.exists_nonzero_mem_of_ne_bot

deleted theorem Ideal.injective_quotient_le_comap_map

deleted theorem Ideal.isMaximal_comap_of_isIntegral_of_isMaximal'

deleted theorem Ideal.isMaximal_comap_of_isIntegral_of_isMaximal

deleted theorem Ideal.isMaximal_of_isIntegral_of_isMaximal_comap'

deleted theorem Ideal.isMaximal_of_isIntegral_of_isMaximal_comap

deleted theorem Ideal.map_eq_top_iff

deleted theorem Ideal.map_eq_top_iff_of_ker_le

deleted theorem Ideal.mem_of_one_mem

added def Ideal.primesOver

deleted theorem Ideal.quotient_mk_maps_eq

deleted def primesOver

deleted theorem primesOver_bot

Modified Mathlib/RingTheory/Ideal/Prime.lean

added def Ideal.primeCompl

Modified Mathlib/RingTheory/Jacobson/Ring.lean

Modified Mathlib/RingTheory/LocalRing/Quotient.lean

Modified Mathlib/RingTheory/Localization/AtPrime.lean

deleted theorem Ideal.disjoint_map_primeCompl_iff_comap_le

deleted def Ideal.primeCompl

deleted theorem Ideal.primeCompl_le_nonZeroDivisors

Modified Mathlib/RingTheory/Spectrum/Prime/Topology.lean

Modified Mathlib/RingTheory/Support.lean

Modified Mathlib/RingTheory/Valuation/ExtendToLocalization.lean

Modified Mathlib/RingTheory/Valuation/LocalSubring.lean