← all areas

Namespace PrimeSpectrum 8 theorems

• Specialisation-invariant functions on a connected Noetherian spectrum are constant PrimeSpectrum.apply_eq_apply_of_forall_le_of_connectedSpace 0 below · cited by 1 · depth 15
• Locally constant functions on Spec R come from complete orthogonal idempotents PrimeSpectrum.exists_completeOrthogonalIdempotents_forall_apply_eq_iff 0 below · cited by 1 · depth 16
• Complete orthogonal idempotents give a locally constant function on Spec R PrimeSpectrum.exists_locallyConstant_forall_apply_eq_iff 0 below · cited by 1 · depth 16
• Difference of idempotent-cut functions on Spec R PrimeSpectrum.forall_sub_apply_eq_iff 0 below · cited by 1 · depth 16
• Convolution identity for idempotents cutting out an additive cocycle PrimeSpectrum.sum_map_mul_map_eq_map_of_forall_comap_add 0 below · cited by 1 · depth 16
• Open, nonempty, maximal-homogeneous subsets of a Jacobson spectrum PrimeSpectrum.eq_univ_of_isOpen_of_nonempty_of_forall_isMaximal 0 below · cited by 2 · depth 19
• Range of Spec of an integral ring map is V(ker) PrimeSpectrum.range_comap_eq_zeroLocus_ker_of_isIntegral 0 below · cited by 1 · depth 28
• Locally constant functions on Spec T refine into idempotents PrimeSpectrum.exists_completeOrthogonalIdempotents_forall_apply_eq_of_isLocallyConstant 0 below · cited by 1 · depth 34