Commit 2025-06-03 14:09 4cdc8929

View on Github →

feat(RingTheory): formulas for Module.rankAtStalk for various constructions (#22341) Compute Module.rankAtStalk for base change and products. Relate it to being trivial and to the dimension of the fiber.

Estimated changes

Modified Mathlib/RingTheory/LocalRing/Module.lean

added theorem Module.mem_support_iff_nontrivial_residueField_tensorProduct

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

added theorem PrimeSpectrum.isEmpty_iff_subsingleton

added theorem PrimeSpectrum.nonempty_iff_nontrivial

added theorem PrimeSpectrum.nontrivial

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

added theorem Module.nontrivial_of_rankAtStalk_pos

added theorem Module.rankAtStalk_baseChange

added theorem Module.rankAtStalk_eq

added theorem Module.rankAtStalk_eq_finrank_of_free

added theorem Module.rankAtStalk_eq_finrank_tensorProduct

added theorem Module.rankAtStalk_eq_of_equiv

added theorem Module.rankAtStalk_eq_zero_iff_notMem_support

added theorem Module.rankAtStalk_eq_zero_iff_subsingleton

added theorem Module.rankAtStalk_eq_zero_of_subsingleton

added theorem Module.rankAtStalk_pi

added theorem Module.rankAtStalk_pos_iff_mem_support

added theorem Module.rankAtStalk_prod

added theorem Module.rankAtStalk_self

added theorem Module.rankAtStalk_tensorProduct

added theorem Module.rankAtStalk_tensorProduct_of_isScalarTower

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

added theorem PrimeSpectrum.nontrivial_iff_mem_rangeComap