Documentation Verification Report

GoingDown

📁 Source: Mathlib/RingTheory/Ideal/GoingDown.lean

Statistics

Metric	Count
Definitions `HasGoingDown`	1
Theorems `exists_ideal_le_liesOver_of_lt`, `iff_generalizingMap_primeSpectrumComap`, `of_comap_localRingHom_surjective`, `of_flat`, `trans`, `exists_ideal_le_liesOver_of_le`, `exists_ideal_lt_liesOver_of_lt`, `exists_ltSeries_of_hasGoingDown`	8
Total	9

Algebra

Definitions

Name	Category	Theorems
`HasGoingDown` 📖	CompData	5 math math: `HasGoingDown.of_comap_localRingHom_surjective`, `instHasGoingDownOfIsDomainOfFaithfulSMulOfIsIntegralOfIsIntegrallyClosed`, `HasGoingDown.trans`, `HasGoingDown.iff_generalizingMap_primeSpectrumComap`, `HasGoingDown.of_flat`

Algebra.HasGoingDown

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_ideal_le_liesOver_of_lt` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.under`	`Preorder.toLE` `Ideal.IsPrime` `Ideal.LiesOver`	—	—
`iff_generalizingMap_primeSpectrumComap` 📖	mathematical	—	`Algebra.HasGoingDown` `GeneralizingMap` `PrimeSpectrum` `CommRing.toCommSemiring` `PrimeSpectrum.zariskiTopology` `PrimeSpectrum.comap` `algebraMap` `CommSemiring.toSemiring`	—	`Ideal.exists_ideal_le_liesOver_of_le` `PrimeSpectrum.isPrime` `Ideal.IsPrime.under` `Ideal.over_under` `PrimeSpectrum.le_iff_specializes` `PrimeSpectrum.ext` `Ideal.LiesOver.over` `LT.lt.le` `RingHom.instRingHomClass`
`of_comap_localRingHom_surjective` 📖	mathematical	`PrimeSpectrum` `Localization.AtPrime` `CommRing.toCommSemiring` `OreLocalization.instCommSemiring` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Ideal.under` `Ideal.IsPrime.under` `PrimeSpectrum.comap` `Localization.localRingHom` `algebraMap` `Ideal`	`Algebra.HasGoingDown`	—	`Ideal.IsPrime.under` `Ideal.isPrime_map_of_isLocalizationAtPrime` `Localization.isLocalization` `LT.lt.le` `Ideal.over_under` `RingHom.instRingHomClass` `Ideal.under_under` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Localization.AtPrime.instIsScalarTower` `IsScalarTower.left` `Ideal.under_map_of_isLocalizationAtPrime`
`of_flat` 📖	mathematical	—	`Algebra.HasGoingDown`	—	`of_comap_localRingHom_surjective` `Ideal.IsPrime.under` `Ideal.over_under` `RingHom.algebraMap_toAlgebra` `Localization.isLocalHom_localRingHom` `Ideal.LiesOver.over` `Module.FaithfullyFlat.of_flat_of_isLocalHom` `Localization.AtPrime.isLocalRing` `instFlatAtPrime` `PrimeSpectrum.comap_surjective_of_faithfullyFlat`
`trans` 📖	mathematical	—	`Algebra.HasGoingDown`	—	`iff_generalizingMap_primeSpectrumComap` `IsScalarTower.algebraMap_eq` `GeneralizingMap.comp`

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_ideal_le_liesOver_of_le` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`IsPrime` `LiesOver`	—	`le_refl` `over_def` `Algebra.HasGoingDown.exists_ideal_le_liesOver_of_lt` `lt_of_le_of_ne`
`exists_ideal_lt_liesOver_of_lt` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`IsPrime` `LiesOver`	—	`exists_ideal_le_liesOver_of_le` `LT.lt.le` `eq_of_le_of_not_lt` `over_def`
`exists_ltSeries_of_hasGoingDown` 📖	mathematical	—	`RelSeries.length` `PrimeSpectrum` `CommRing.toCommSemiring` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `PrimeSpectrum.instPartialOrder` `RelSeries.last` `IsPrime` `CommSemiring.toSemiring` `PrimeSpectrum.comap` `algebraMap` `RelSeries.toList`	—	`RelSeries.last_singleton` `RelSeries.toList_singleton` `PrimeSpectrum.ext` `LiesOver.over` `RelSeries.last_cons` `RelSeries.toList_getElem_zero_eq_head` `RingHom.instRingHomClass` `under_def` `RelSeries.length_toList` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instNoMaxOrder` `Nat.instCanonicallyOrderedAdd` `List.getElem_map_rev` `PrimeSpectrum.ext_iff` `exists_ideal_lt_liesOver_of_lt` `PrimeSpectrum.isPrime` `RelSeries.cons_length` `RelSeries.toList_cons`

---

← Back to Index