Theorems · Definition · commutative algebra
Module.support
(R : Type u_1) → (M : Type u_2) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [Module R M] → Set (PrimeSpectrum R)
The support of a module, defined as the set of primes p such that Mₚ ≠ 0.
- Defined in
- Mathlib.RingTheory.Support
- Cited by
- 52 results in Mathlib
- Foundations
- Depth 31 from the axioms · uses propext, Quot.sound
- Assumes
- CommRingAddCommGroupModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Modulestatement and proof · cited by 20,661
- CommRingstatement and proof · cited by 17,173
- AddCommGroupstatement and proof · cited by 12,871
- Set.ofPredproof · cited by 6,101
- Nontrivialproof · cited by 2,416
- PrimeSpectrumstatement and proof · cited by 625
- Ideal.primeComplproof · cited by 462
- PrimeSpectrum.asIdealproof · cited by 333
- LocalizedModuleproof · cited by 154
Cited by53
Results whose statement or proof uses this declaration.
- Module.supportDimproof · cited by 23
- Module.support_eq_zeroLocusstatement · cited by 10
- LocalizedModule.subsingleton_iff_support_subsetstatement and proof · cited by 5
- Module.support_eq_empty_iffstatement and proof · cited by 5
- Module.mem_support_iff_exists_annihilatorstatement · cited by 4
- Module.mem_support_iff_of_finitestatement · cited by 4
- Module.mem_support_monostatement and proof · cited by 4
- Module.support_subset_of_surjectivestatement · cited by 4
- Module.mem_support_iffstatement · cited by 3
- Module.support_subset_of_injectivestatement · cited by 3
- Algebra.unramifiedLocus_eq_compl_supportstatement and proof · cited by 3
- Algebra.basicOpen_subset_etaleLocus_iffproof · cited by 3