Commit 2024-07-22 15:39 d6c2f3ec

View on Github →

feat(RingTheory/Support): Define support of a module (#14507) We define the support of a module as a Set (PrimeSpectrum R). We prove various results about it including Supp M = ∅ ↔ M = 0 and that Supp M is closed for finite modules.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/LocalizedModule.lean

added theorem LocalizedModule.mem_ker_mkLinearMap_iff

added theorem LocalizedModule.subsingleton_iff

added theorem LocalizedModule.subsingleton_iff_ker_eq_top

Created Mathlib/AlgebraicGeometry/PrimeSpectrum/Module.lean

added theorem LocalizedModule.subsingleton_iff_disjoint

added theorem Module.isClosed_support

added theorem Module.stableUnderSpecialization_support

added theorem Module.support_subset_preimage_comap

Created Mathlib/RingTheory/Support.lean

added theorem LinearEquiv.support_eq

added theorem LocalizedModule.exists_subsingleton_away

added theorem LocalizedModule.subsingleton_iff_support_subset

added theorem Module.annihilator_le_of_mem_support

added theorem Module.mem_support_iff'

added theorem Module.mem_support_iff

added theorem Module.mem_support_iff_exists_annihilator

added theorem Module.mem_support_iff_of_finite

added theorem Module.mem_support_iff_of_span_eq_top

added theorem Module.not_mem_support_iff'

added theorem Module.not_mem_support_iff

added def Module.support

added theorem Module.support_eq_empty

added theorem Module.support_eq_empty_iff

added theorem Module.support_eq_zeroLocus

added theorem Module.support_of_algebra

added theorem Module.support_of_exact

added theorem Module.support_of_noZeroSMulDivisors

added theorem Module.support_subset_of_injective

added theorem Module.support_subset_of_surjective