Commit 2026-01-16 14:47 95093e96

View on Github →

feat(RingTheory/Ideal): generalize Submodule.colon to sets (#33390) This PR generalizes Submodule.colon to arguments of type Set M in the second slot and updates the surrounding API accordingly. Main changes

  • Generalize Submodule.colon to take S : Set M rather than P : Submodule R M.
  • Normalize theorems/lemmas to use Set.univ instead of ⊤ where appropriate.
  • Strengthen iInf_colon_iSup by removing an unnecessary commutativity assumption.
  • Update monotonicity and inclusion lemmas (e.g. _root_.Ideal.le_colon) to use set inclusions.
  • Add colon_bot' (CommSemiring): identify ⊥.colon S with the annihilator of Submodule.span R S.
  • Adjust annihilator-related proofs to account for the generalized colon, using explicit coercions such as Submodule.top_coe.

Estimated changes

added theorem Ideal.colon_span
modified theorem Ideal.le_colon
deleted theorem Ideal.mem_colon_singleton
added theorem Submodule.bot_colon'
added theorem Submodule.bot_colon
modified def Submodule.colon
deleted theorem Submodule.colon_bot
added theorem Submodule.colon_empty
added theorem Submodule.colon_iUnion
modified theorem Submodule.colon_mono
added theorem Submodule.colon_span
deleted theorem Submodule.colon_top
added theorem Submodule.colon_union
added theorem Submodule.colon_univ
added theorem Submodule.iInf_colon
deleted theorem Submodule.iInf_colon_iSup
added theorem Submodule.inf_colon
modified theorem Submodule.mem_colon'
modified theorem Submodule.mem_colon
added theorem Submodule.top_colon