Commit 2026-02-09 11:07 2c706fb9

View on Github →

feat(RingTheory): local structure for finite unramified algebras (#34928)

Estimated changes

Modified Mathlib/RingTheory/Ideal/GoingUp.lean

added theorem Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton

Modified Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean

Modified Mathlib/RingTheory/QuasiFinite/Basic.lean

added theorem Ideal.Fiber.lift_residueField_surjective

Modified Mathlib/RingTheory/Unramified/LocalRing.lean

modified theorem Algebra.isUnramifiedAt_iff_map_eq

added theorem Localization.exists_awayMap_bijective_of_localRingHom_bijective

added theorem Localization.exists_awayMap_bijective_of_residueField_surjective

added theorem Localization.exists_awayMap_injective_of_localRingHom_injective

added theorem Localization.finite_of_primesOver_eq_singleton

added theorem Localization.localRingHom_injective_of_primesOver_eq_singleton

added theorem Localization.localRingHom_surjective_of_primesOver_eq_singleton

Modified Mathlib/RingTheory/Unramified/LocalStructure.lean

added theorem Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionAt_of_finite

added theorem Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top

added theorem Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective

Modified Mathlib/RingTheory/Unramified/Locus.lean