Support

📁 Source: Mathlib/RingTheory/Support.lean

Statistics

Metric	Count
Definitions `support`	1
Theorems `exists_subsingleton_away`, `support_eq`, `exists_subsingleton_away`, `subsingleton_iff_support_subset`, `annihilator_le_of_mem_support`, `mem_support_iff`, `mem_support_iff'`, `mem_support_iff_exists_annihilator`, `mem_support_iff_of_finite`, `mem_support_iff_of_span_eq_top`, `mem_support_mono`, `nonempty_support_iff`, `nonempty_support_of_nontrivial`, `notMem_support_iff`, `notMem_support_iff'`, `support_eq_empty`, `support_eq_empty_iff`, `support_eq_zeroLocus`, `support_of_algebra`, `support_of_exact`, `support_of_noZeroSMulDivisors`, `support_quotSMulTop`, `support_quotient`, `support_subset_of_injective`, `support_subset_of_surjective`	25
Total	26

IsLocalizedModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_subsingleton_away` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `LocalizedModule` `Submonoid.powers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommGroup.toAddCommMonoid`	—	`RingHomInvPair.ids` `IsScalarTower.left` `IsScalarTower.right` `Equiv.subsingleton` `LocalizedModule.exists_subsingleton_away`

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`support_eq` 📖	mathematical	—	`Module.support`	—	`RingHomInvPair.ids` `HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Module.support_subset_of_injective` `injective` `Module.support_subset_of_surjective` `surjective`

LocalizedModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_subsingleton_away` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `LocalizedModule` `Submonoid.powers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommGroup.toAddCommMonoid`	—	`PrimeSpectrum.isPrime` `Set.mem_iUnion₂` `Set.compl_iInter₂` `PrimeSpectrum.zeroLocus_iUnion₂` `Set.biUnion_of_singleton` `Module.support_eq_zeroLocus` `subsingleton_iff` `Submonoid.mem_powers` `Module.mem_annihilator`
`subsingleton_iff_support_subset` 📖	mathematical	—	`LocalizedModule` `CommRing.toCommSemiring` `Submonoid.powers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set` `PrimeSpectrum` `Set.instHasSubset` `Module.support` `PrimeSpectrum.zeroLocus` `Set.instSingletonSet`	—	`subsingleton_iff` `Module.mem_support_iff_exists_annihilator` `Ideal.IsPrime.mem_of_pow_mem` `PrimeSpectrum.isPrime` `Submodule.mem_annihilator_span_singleton` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `one_smul` `Submodule.span_singleton_eq_bot` `Submodule.annihilator_eq_top_iff` `Ideal.radical_eq_sInf` `Ideal.mem_sInf`

Module

Definitions

Name	Category	Theorems
`support` 📖	CompOp	35 math math: `support_quotient`, `LocalizedModule.subsingleton_iff_disjoint`, `LinearEquiv.support_eq`, `rankAtStalk_eq_zero_iff_notMem_support`, `mem_support_iff_of_finite`, `support_eq_empty`, `support_subset_preimage_comap`, `support_of_algebra`, `Algebra.unramifiedLocus_eq_compl_support`, `mem_support_iff_exists_annihilator`, `mem_support_iff'`, `support_of_exact`, `IsLocalRing.closedPoint_mem_support`, `mem_support_mono`, `support_eq_empty_iff`, `rankAtStalk_pos_iff_mem_support`, `nonempty_support_of_nontrivial`, `support_quotSMulTop`, `LocalizedModule.subsingleton_iff_support_subset`, `mem_support_iff_nontrivial_residueField_tensorProduct`, `support_of_supportDim_eq_zero`, `notMem_support_iff`, `support_of_noZeroSMulDivisors`, `exists_ltSeries_support_isMaximal_last_of_ltSeries_support`, `support_subset_of_injective`, `mem_support_iff`, `nonempty_support_iff`, `support_eq_zeroLocus`, `stableUnderSpecialization_support`, `Algebra.smoothLocus_eq_compl_support_inter`, `isClosed_support`, `mem_support_iff_of_span_eq_top`, `support_subset_of_surjective`, `Algebra.etaleLocus_eq_compl_support`, `notMem_support_iff'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`annihilator_le_of_mem_support` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `annihilator` `AddCommGroup.toAddCommMonoid` `PrimeSpectrum.asIdeal`	—	`mem_support_iff_exists_annihilator` `le_trans` `LinearMap.annihilator_le_of_injective` `Subtype.val_injective`
`mem_support_iff` 📖	mathematical	—	`PrimeSpectrum` `CommRing.toCommSemiring` `Set` `Set.instMembership` `support` `Nontrivial` `LocalizedModule` `Ideal.primeCompl` `CommSemiring.toSemiring` `PrimeSpectrum.asIdeal` `PrimeSpectrum.isPrime` `AddCommGroup.toAddCommMonoid`	—	—
`mem_support_iff'` 📖	mathematical	—	`PrimeSpectrum` `CommRing.toCommSemiring` `Set` `Set.instMembership` `support`	—	`notMem_support_iff'` `Mathlib.Tactic.Push.not_forall_eq` `Mathlib.Tactic.Push.not_and_eq`
`mem_support_iff_exists_annihilator` 📖	mathematical	—	`PrimeSpectrum` `CommRing.toCommSemiring` `Set` `Set.instMembership` `support` `Ideal` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.annihilator` `AddCommGroup.toAddCommMonoid` `Submodule.span` `Set.instSingletonSet` `PrimeSpectrum.asIdeal`	—	`mem_support_iff'` `instIsConcreteLE`
`mem_support_iff_of_finite` 📖	mathematical	—	`PrimeSpectrum` `CommRing.toCommSemiring` `Set` `Set.instMembership` `support` `Ideal` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `annihilator` `AddCommGroup.toAddCommMonoid` `PrimeSpectrum.asIdeal`	—	`annihilator_le_of_mem_support` `mem_support_iff_of_span_eq_top` `instIsConcreteLE` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_eq` `Mathlib.Tactic.Push.not_forall_eq` `Submodule.annihilator_top` `Submodule.mem_annihilator_span` `Finset.dvd_prod_of_mem` `Finset.mem_attach` `mul_comm` `SemigroupAction.mul_smul` `smul_zero` `Submonoid.prod_mem` `PrimeSpectrum.isPrime` `Subtype.forall'`
`mem_support_iff_of_span_eq_top` 📖	mathematical	`Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Top.top` `Submodule` `Submodule.instTop`	`PrimeSpectrum` `Set` `Set.instMembership` `support` `Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.annihilator` `Set.instSingletonSet` `PrimeSpectrum.asIdeal`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `PrimeSpectrum.isPrime` `notMem_support_iff` `IsScalarTower.left` `IsScalarTower.right` `LocalizedModule.subsingleton_iff_ker_eq_top` `top_le_iff` `Submodule.span_le` `Set.subset_def` `instIsConcreteLE` `Mathlib.Tactic.Push.not_and_eq` `Mathlib.Tactic.Push.not_forall_eq` `mem_support_iff_exists_annihilator`
`mem_support_mono` 📖	mathematical	`PrimeSpectrum` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `PrimeSpectrum.instPartialOrder`	`Set` `Set.instMembership` `support`	—	`mem_support_iff_exists_annihilator` `LE.le.trans`
`nonempty_support_iff` 📖	mathematical	—	`Set.Nonempty` `PrimeSpectrum` `CommRing.toCommSemiring` `support` `Nontrivial`	—	`Set.nonempty_iff_ne_empty` `support_eq_empty_iff` `not_subsingleton_iff_nontrivial`
`nonempty_support_of_nontrivial` 📖	mathematical	—	`Set.Nonempty` `PrimeSpectrum` `CommRing.toCommSemiring` `support`	—	`nonempty_support_iff`
`notMem_support_iff` 📖	mathematical	—	`PrimeSpectrum` `CommRing.toCommSemiring` `Set` `Set.instMembership` `support` `LocalizedModule` `Ideal.primeCompl` `CommSemiring.toSemiring` `PrimeSpectrum.asIdeal` `PrimeSpectrum.isPrime` `AddCommGroup.toAddCommMonoid`	—	`not_nontrivial_iff_subsingleton`
`notMem_support_iff'` 📖	mathematical	—	`PrimeSpectrum` `CommRing.toCommSemiring` `Set` `Set.instMembership` `support` `Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `PrimeSpectrum.asIdeal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`PrimeSpectrum.isPrime` `Ideal.one_notMem`
`support_eq_empty` 📖	mathematical	—	`support` `Set` `PrimeSpectrum` `CommRing.toCommSemiring` `Set.instEmptyCollection`	—	`support_eq_empty_iff`
`support_eq_empty_iff` 📖	mathematical	—	`support` `Set` `PrimeSpectrum` `CommRing.toCommSemiring` `Set.instEmptyCollection`	—	`Set.subset_empty_iff` `PrimeSpectrum.zeroLocus_singleton_one` `LocalizedModule.subsingleton_iff_support_subset` `LocalizedModule.subsingleton_iff` `Submonoid.powers_one` `one_smul`
`support_eq_zeroLocus` 📖	mathematical	—	`support` `PrimeSpectrum.zeroLocus` `CommRing.toCommSemiring` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `annihilator` `AddCommGroup.toAddCommMonoid`	—	`Set.ext` `mem_support_iff_of_finite`
`support_of_algebra` 📖	mathematical	—	`support` `Ring.toAddCommGroup` `Algebra.toModule` `CommRing.toCommSemiring` `Ring.toSemiring` `PrimeSpectrum.zeroLocus` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `RingHom` `RingHom.instFunLike` `RingHom.instRingHomClass` `algebraMap`	—	`Set.ext` `RingHom.instRingHomClass` `instIsConcreteLE` `Algebra.smul_def` `MulZeroClass.zero_mul` `Algebra.algebraMap_eq_smul_one`
`support_of_exact` 📖	mathematical	`Function.Exact` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`support` `Set` `PrimeSpectrum` `Set.instUnion`	—	`subset_antisymm` `Set.instAntisymmSubset` `Mathlib.Tactic.Contrapose.contrapose₁` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Submonoid.mul_mem` `PrimeSpectrum.isPrime` `SemigroupAction.mul_smul` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `Set.union_subset` `support_subset_of_injective` `support_subset_of_surjective`
`support_of_noZeroSMulDivisors` 📖	mathematical	—	`support` `Set.univ` `PrimeSpectrum` `CommRing.toCommSemiring`	—	`IsDomain.toIsCancelMulZero` `exists_ne` `Ideal.zero_mem`
`support_quotSMulTop` 📖	mathematical	—	`support` `QuotSMulTop` `Submodule.Quotient.addCommGroup` `CommRing.toRing` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Submodule.pointwiseAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Submodule.pointwiseDistribMulAction` `toDistribMulAction` `Top.top` `Submodule.instTop` `Submodule.Quotient.module` `Set` `PrimeSpectrum` `Set.instInter` `PrimeSpectrum.zeroLocus` `Set.instSingletonSet`	—	`smulCommClass_self` `IsScalarTower.left` `LinearEquiv.support_eq` `Submodule.ideal_span_singleton_smul` `support_quotient` `PrimeSpectrum.zeroLocus_span`
`support_quotient` 📖	mathematical	—	`support` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `CommRing.toRing` `Ideal` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `toDistribMulAction` `Top.top` `Submodule.instTop` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Set` `PrimeSpectrum` `Set.instInter` `PrimeSpectrum.zeroLocus` `SetLike.coe` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`subset_antisymm` `IsScalarTower.left` `Set.instAntisymmSubset` `Set.subset_inter` `support_subset_of_surjective` `Submodule.mkQ_surjective` `support_eq_zeroLocus` `Finite.quotient` `PrimeSpectrum.zeroLocus_anti_mono_ideal` `Submodule.annihilator_quotient` `Submodule.mem_colon` `Submodule.smul_mem_smul` `PrimeSpectrum.isPrime` `mem_support_iff` `RingHomInvPair.ids` `RingHomCompTriple.ids` `Localization.isLocalization` `localizedModuleIsLocalizedModule` `Submodule.localized.eq_1` `IsScalarTower.right` `instIsLocalizedModuleLinearMapOfIsLocalization` `Submodule.localized'_smul` `Ideal.localized'_eq_map` `Submodule.localized'_top` `Submodule.Quotient.nontrivial_iff` `Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator` `Finite.instLocalizationLocalizedModule` `trans` `Localization.AtPrime.isLocalRing` `instIsTransLe` `Localization.AtPrime.map_eq_maximalIdeal` `Ideal.map_mono` `IsLocalRing.maximalIdeal_le_jacobson` `Equiv.nontrivial`
`support_subset_of_injective` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`Set` `PrimeSpectrum` `Set.instHasSubset` `support`	—	`map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass`
`support_subset_of_surjective` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`Set` `PrimeSpectrum` `Set.instHasSubset` `support`	—	`map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass`

---

← Back to Index