Commit 2026-01-06 11:03 266ae78a

View on Github →

feat(RingTheory): construct etale neighborhood that isolates point in fiber (#32823)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Polynomial/Monic.lean

Created Mathlib/RingTheory/Etale/QuasiFinite.lean

added theorem Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq

added theorem Ideal.comap_fiberIsoOfBijectiveResidueField_apply

added theorem Ideal.comap_fiberIsoOfBijectiveResidueField_symm

added theorem Ideal.eq_of_comap_eq_comap_of_bijective_residueFieldMap

added theorem Ideal.exists_not_mem_forall_mem_of_ne_of_liesOver

added def Ideal.fiberIsoOfBijectiveResidueField

Modified Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean

added theorem Algebra.exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime.{u}

added theorem Polynomial.UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijective

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

added theorem IsArtinianRing.exists_not_mem_forall_mem_of_ne

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

added theorem PrimeSpectrum.comapEquiv_symm

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

added theorem PrimeSpectrum.toPiLocalization_bijective