Documentation Verification Report

Localization

📁 Source: Mathlib/RingTheory/Spectrum/Maximal/Localization.lean

Statistics

Metric	Count
Definitions `PiLocalization`, `mapPiLocalization`, `toPiLocalization`, `PiLocalization`, `mapPiLocalization`, `piLocalizationToMaximal`, `piLocalizationToMaximalEquiv`, `toPiLocalization`	8
Theorems `finite_of_toPiLocalization_pi_surjective`, `finite_of_toPiLocalization_surjective`, `iInf_localization_eq_bot`, `mapPiLocalization_bijective`, `mapPiLocalization_comp`, `mapPiLocalization_id`, `mapPiLocalization_naturality`, `toPiLocalization_apply_apply`, `toPiLocalization_injective`, `toPiLocalization_not_surjective_of_infinite`, `finite_of_toPiLocalization_pi_surjective`, `finite_of_toPiLocalization_surjective`, `iInf_localization_eq_bot`, `isMaximal_of_toPiLocalization_surjective`, `mapPiLocalization_bijective`, `mapPiLocalization_comp`, `mapPiLocalization_id`, `mapPiLocalization_naturality`, `piLocalizationToMaximal_bijective`, `piLocalizationToMaximal_comp_toPiLocalization`, `piLocalizationToMaximal_surjective`, `toPiLocalization_injective`, `toPiLocalization_not_surjective_of_infinite`	23
Total	31

MaximalSpectrum

Definitions

Name	Category	Theorems
`PiLocalization` 📖	CompOp	11 math math: `mapPiLocalization_bijective`, `toPiLocalization_apply_apply`, `mapPiLocalization_naturality`, `mapPiLocalization_id`, `PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalization`, `PrimeSpectrum.piLocalizationToMaximal_surjective`, `mapPiLocalization_comp`, `toPiLocalization_injective`, `toPiLocalization_not_surjective_of_infinite`, `PrimeSpectrum.piLocalizationToMaximal_bijective`, `PrimeSpectrum.maximalSpectrumToPiLocalization_surjective_of_discreteTopology`
`mapPiLocalization` 📖	CompOp	4 math math: `mapPiLocalization_bijective`, `mapPiLocalization_naturality`, `mapPiLocalization_id`, `mapPiLocalization_comp`
`toPiLocalization` 📖	CompOp	6 math math: `toPiLocalization_apply_apply`, `mapPiLocalization_naturality`, `PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalization`, `toPiLocalization_injective`, `toPiLocalization_not_surjective_of_infinite`, `PrimeSpectrum.maximalSpectrumToPiLocalization_surjective_of_discreteTopology`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_of_toPiLocalization_pi_surjective` 📖	mathematical	`Nontrivial` `PiLocalization` `Pi.commSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Pi.nonAssocSemiring` `MaximalSpectrum` `Localization.AtPrime` `asIdeal` `OreLocalization.instSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `RingHom.instFunLike` `toPiLocalization`	`Finite`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `toPiLocalization_not_surjective_of_infinite`
`finite_of_toPiLocalization_surjective` 📖	mathematical	`PiLocalization` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Pi.nonAssocSemiring` `MaximalSpectrum` `Localization.AtPrime` `asIdeal` `OreLocalization.instSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `RingHom.instFunLike` `toPiLocalization`	`Finite`	—	`toPiLocalization_injective` `mapPiLocalization_bijective` `finite_of_toPiLocalization_pi_surjective` `IsLocalRing.toNontrivial` `Localization.AtPrime.isLocalRing` `Ideal.IsMaximal.isPrime'` `isMaximal` `Function.Surjective.of_comp` `RingHom.coe_comp` `mapPiLocalization_naturality`
`iInf_localization_eq_bot` 📖	mathematical	—	`iInf` `Subalgebra` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MaximalSpectrum` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `Localization.subalgebra.ofField` `Ideal.primeCompl` `CommSemiring.toSemiring` `asIdeal` `Ideal.IsMaximal.isPrime'` `isMaximal` `Ideal.primeCompl_le_nonZeroDivisors` `IsDomain.to_noZeroDivisors` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`Subalgebra.ext` `Ideal.IsMaximal.isPrime'` `isMaximal` `Ideal.primeCompl_le_nonZeroDivisors` `IsDomain.to_noZeroDivisors` `Algebra.mem_bot` `Algebra.mem_iInf` `Mathlib.Tactic.Contrapose.contrapose₁` `one_smul` `Ideal.exists_le_maximal` `Ideal.ne_top_iff_one` `Algebra.smul_def` `mul_one` `mul_left_comm` `mul_inv_cancel₀` `map_ne_zero_iff` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsFractionRing.injective` `Ideal.zero_mem` `Ideal.IsMaximal.ne_top` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `inv_one`
`mapPiLocalization_bijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike`	`PiLocalization` `Pi.nonAssocSemiring` `MaximalSpectrum` `Localization.AtPrime` `asIdeal` `OreLocalization.instSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `mapPiLocalization`	—	`RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingEquiv.bijective` `Function.Bijective.comp` `mapPiLocalization_comp` `RingEquiv.comp_symm` `mapPiLocalization.congr_simp` `mapPiLocalization_id` `RingEquiv.symm_comp`
`mapPiLocalization_comp` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike`	`mapPiLocalization` `RingHom.comp` `Function.Bijective.comp` `PiLocalization` `Pi.nonAssocSemiring` `MaximalSpectrum` `Localization.AtPrime` `asIdeal` `OreLocalization.instSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid`	—	`RingHom.ext` `Function.Bijective.comp` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `Ideal.IsMaximal.isPrime'` `isMaximal` `Localization.localRingHom_comp`
`mapPiLocalization_id` 📖	mathematical	—	`mapPiLocalization` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Function.bijective_id` `PiLocalization` `Pi.nonAssocSemiring` `MaximalSpectrum` `Localization.AtPrime` `asIdeal` `OreLocalization.instSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid`	—	`RingHom.ext` `Function.bijective_id` `RingHom.instRingHomClass` `Ideal.comap_id` `Localization.localRingHom_id`
`mapPiLocalization_naturality` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike`	`RingHom.comp` `PiLocalization` `Pi.nonAssocSemiring` `MaximalSpectrum` `Localization.AtPrime` `asIdeal` `OreLocalization.instSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `mapPiLocalization` `toPiLocalization`	—	`RingHom.ext` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `Ideal.IsMaximal.isPrime'` `isMaximal` `Localization.isLocalization` `IsLocalization.mk'_one` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Localization.le_comap_primeCompl_iff` `ge_of_eq` `Localization.localRingHom_mk'` `map_one` `MonoidHomClass.toOneHomClass` `IsLocalization.mk'.congr_simp`
`toPiLocalization_apply_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `PiLocalization` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Pi.nonAssocSemiring` `MaximalSpectrum` `Localization.AtPrime` `asIdeal` `OreLocalization.instSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `RingHom.instFunLike` `toPiLocalization` `algebraMap` `OreLocalization.instAlgebra` `Algebra.id`	—	—
`toPiLocalization_injective` 📖	mathematical	—	`PiLocalization` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Pi.nonAssocSemiring` `MaximalSpectrum` `Localization.AtPrime` `asIdeal` `OreLocalization.instSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `RingHom.instFunLike` `toPiLocalization`	—	`one_mul` `Ideal.exists_le_maximal` `Ideal.ne_top_iff_one` `Ideal.IsMaximal.isPrime'` `IsLocalization.eq_iff_exists` `Localization.isLocalization`
`toPiLocalization_not_surjective_of_infinite` 📖	mathematical	`Nontrivial`	`PiLocalization` `Pi.commSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Pi.nonAssocSemiring` `MaximalSpectrum` `Localization.AtPrime` `asIdeal` `OreLocalization.instSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `RingHom.instFunLike` `toPiLocalization`	—	`Ideal.IsMaximal.isPrime'` `PrimeSpectrum.exists_maximal_notMem_range_sigmaToPi_of_infinite` `toPiLocalization_injective` `RingHom.instRingHomClass` `Ideal.IsMaximal.comap_piEvalRingHom` `isMaximal` `Ideal.IsPrime.comap` `Function.update_of_ne` `Ideal.IsMaximal.isPrime` `PrimeSpectrum.ext` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `zero_ne_one` `NeZero.one` `IsLocalRing.toNontrivial` `Localization.AtPrime.isLocalRing` `Function.update_self`

PrimeSpectrum

Definitions

Name	Category	Theorems
`PiLocalization` 📖	CompOp	13 math math: `mapPiLocalization_id`, `toPiLocalization_surjective_of_discreteTopology`, `mapPiLocalization_bijective`, `toPiLocalization_not_surjective_of_infinite`, `mapPiLocalization_comp`, `mapPiLocalization_naturality`, `toPiLocalization_bijective`, `discreteTopology_iff_toPiLocalization_surjective`, `piLocalizationToMaximal_comp_toPiLocalization`, `piLocalizationToMaximal_surjective`, `piLocalizationToMaximal_bijective`, `toPiLocalization_injective`, `discreteTopology_iff_toPiLocalization_bijective`
`mapPiLocalization` 📖	CompOp	4 math math: `mapPiLocalization_id`, `mapPiLocalization_bijective`, `mapPiLocalization_comp`, `mapPiLocalization_naturality`
`piLocalizationToMaximal` 📖	CompOp	3 math math: `piLocalizationToMaximal_comp_toPiLocalization`, `piLocalizationToMaximal_surjective`, `piLocalizationToMaximal_bijective`
`piLocalizationToMaximalEquiv` 📖	CompOp	—
`toPiLocalization` 📖	CompOp	8 math math: `toPiLocalization_surjective_of_discreteTopology`, `toPiLocalization_not_surjective_of_infinite`, `mapPiLocalization_naturality`, `toPiLocalization_bijective`, `discreteTopology_iff_toPiLocalization_surjective`, `piLocalizationToMaximal_comp_toPiLocalization`, `toPiLocalization_injective`, `discreteTopology_iff_toPiLocalization_bijective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_of_toPiLocalization_pi_surjective` 📖	mathematical	`Nontrivial` `PiLocalization` `Pi.commSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Pi.nonAssocSemiring` `PrimeSpectrum` `Localization` `CommSemiring.toCommMonoid` `Ideal.primeCompl` `asIdeal` `isPrime` `OreLocalization.instSemiring` `OreLocalization.oreSetComm` `RingHom.instFunLike` `toPiLocalization`	`Finite`	—	`isPrime` `Mathlib.Tactic.Contrapose.contrapose₁` `toPiLocalization_not_surjective_of_infinite`
`finite_of_toPiLocalization_surjective` 📖	mathematical	`PiLocalization` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Pi.nonAssocSemiring` `PrimeSpectrum` `Localization` `CommSemiring.toCommMonoid` `Ideal.primeCompl` `asIdeal` `isPrime` `OreLocalization.instSemiring` `OreLocalization.oreSetComm` `RingHom.instFunLike` `toPiLocalization`	`Finite`	—	`isPrime` `mapPiLocalization_bijective` `toPiLocalization_injective` `finite_of_toPiLocalization_pi_surjective` `IsLocalRing.toNontrivial` `Localization.AtPrime.isLocalRing` `Function.Surjective.of_comp` `RingHom.coe_comp` `mapPiLocalization_naturality`
`iInf_localization_eq_bot` 📖	mathematical	—	`iInf` `Subalgebra` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `PrimeSpectrum` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `Localization.subalgebra.ofField` `Ideal.primeCompl` `CommSemiring.toSemiring` `asIdeal` `isPrime` `Ideal.primeCompl_le_nonZeroDivisors` `IsDomain.to_noZeroDivisors` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`bot_unique` `isPrime` `Ideal.primeCompl_le_nonZeroDivisors` `IsDomain.to_noZeroDivisors` `LE.le.trans` `Ideal.IsMaximal.isPrime'` `MaximalSpectrum.isMaximal` `Ideal.IsMaximal.isPrime` `Eq.le` `MaximalSpectrum.iInf_localization_eq_bot`
`isMaximal_of_toPiLocalization_surjective` 📖	mathematical	`PiLocalization` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Pi.nonAssocSemiring` `PrimeSpectrum` `Localization` `CommSemiring.toCommMonoid` `Ideal.primeCompl` `asIdeal` `isPrime` `OreLocalization.instSemiring` `OreLocalization.oreSetComm` `RingHom.instFunLike` `toPiLocalization`	`Ideal.IsMaximal`	—	`isPrime` `Ideal.exists_le_maximal` `Ideal.IsPrime.ne_top` `Ideal.IsMaximal.isPrime` `Function.update_self` `one_ne_zero` `NeZero.one` `IsLocalRing.toNontrivial` `Localization.AtPrime.isLocalRing` `Function.update_of_ne` `Ideal.IsMaximal.isPrime'` `Localization.isLocalization` `IsLocalization.map_units` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsLocalization.lift_eq`
`mapPiLocalization_bijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike`	`PiLocalization` `Pi.nonAssocSemiring` `PrimeSpectrum` `Localization` `CommSemiring.toCommMonoid` `Ideal.primeCompl` `asIdeal` `isPrime` `OreLocalization.instSemiring` `OreLocalization.oreSetComm` `mapPiLocalization`	—	`RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `isPrime` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `mapPiLocalization_comp` `RingEquiv.comp_symm` `mapPiLocalization_id` `RingEquiv.symm_comp` `RingEquiv.bijective`
`mapPiLocalization_comp` 📖	mathematical	—	`mapPiLocalization` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `PiLocalization` `Pi.nonAssocSemiring` `PrimeSpectrum` `Localization` `CommSemiring.toCommMonoid` `Ideal.primeCompl` `asIdeal` `isPrime` `OreLocalization.instSemiring` `OreLocalization.oreSetComm`	—	`RingHom.ext` `isPrime` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `Localization.localRingHom_comp`
`mapPiLocalization_id` 📖	mathematical	—	`mapPiLocalization` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `PiLocalization` `Pi.nonAssocSemiring` `PrimeSpectrum` `Localization` `CommSemiring.toCommMonoid` `Ideal.primeCompl` `asIdeal` `isPrime` `OreLocalization.instSemiring` `OreLocalization.oreSetComm`	—	`RingHom.ext` `isPrime` `RingHom.instRingHomClass` `Ideal.comap_id` `Localization.localRingHom_id`
`mapPiLocalization_naturality` 📖	mathematical	—	`RingHom.comp` `PiLocalization` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Pi.nonAssocSemiring` `PrimeSpectrum` `Localization` `CommSemiring.toCommMonoid` `Ideal.primeCompl` `asIdeal` `isPrime` `OreLocalization.instSemiring` `OreLocalization.oreSetComm` `mapPiLocalization` `toPiLocalization`	—	`RingHom.ext` `isPrime` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `Localization.isLocalization` `IsLocalization.mk'_one` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Localization.le_comap_primeCompl_iff` `ge_of_eq` `Localization.localRingHom_mk'` `map_one` `MonoidHomClass.toOneHomClass` `IsLocalization.mk'.congr_simp`
`piLocalizationToMaximal_bijective` 📖	mathematical	`Ideal.IsMaximal` `CommSemiring.toSemiring`	`Function.Bijective` `PiLocalization` `MaximalSpectrum.PiLocalization` `DFunLike.coe` `RingHom` `Pi.nonAssocSemiring` `PrimeSpectrum` `Localization` `CommSemiring.toCommMonoid` `Ideal.primeCompl` `asIdeal` `isPrime` `Semiring.toNonAssocSemiring` `OreLocalization.instSemiring` `OreLocalization.oreSetComm` `MaximalSpectrum` `Localization.AtPrime` `MaximalSpectrum.asIdeal` `RingHom.instFunLike` `piLocalizationToMaximal`	—	`RingEquiv.bijective` `isPrime`
`piLocalizationToMaximal_comp_toPiLocalization` 📖	mathematical	—	`RingHom.comp` `PiLocalization` `MaximalSpectrum.PiLocalization` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Pi.nonAssocSemiring` `PrimeSpectrum` `Localization` `CommSemiring.toCommMonoid` `Ideal.primeCompl` `asIdeal` `isPrime` `OreLocalization.instSemiring` `OreLocalization.oreSetComm` `MaximalSpectrum` `Localization.AtPrime` `MaximalSpectrum.asIdeal` `piLocalizationToMaximal` `toPiLocalization` `MaximalSpectrum.toPiLocalization`	—	`isPrime`
`piLocalizationToMaximal_surjective` 📖	mathematical	—	`PiLocalization` `MaximalSpectrum.PiLocalization` `DFunLike.coe` `RingHom` `Pi.nonAssocSemiring` `PrimeSpectrum` `Localization` `CommSemiring.toCommMonoid` `Ideal.primeCompl` `CommSemiring.toSemiring` `asIdeal` `isPrime` `Semiring.toNonAssocSemiring` `OreLocalization.instSemiring` `OreLocalization.oreSetComm` `MaximalSpectrum` `Localization.AtPrime` `MaximalSpectrum.asIdeal` `RingHom.instFunLike` `piLocalizationToMaximal`	—	`isPrime` `MaximalSpectrum.isMaximal`
`toPiLocalization_injective` 📖	mathematical	—	`PiLocalization` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Pi.nonAssocSemiring` `PrimeSpectrum` `Localization` `CommSemiring.toCommMonoid` `Ideal.primeCompl` `asIdeal` `isPrime` `OreLocalization.instSemiring` `OreLocalization.oreSetComm` `RingHom.instFunLike` `toPiLocalization`	—	`isPrime` `MaximalSpectrum.toPiLocalization_injective`
`toPiLocalization_not_surjective_of_infinite` 📖	mathematical	`Nontrivial`	`PiLocalization` `Pi.commSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Pi.nonAssocSemiring` `PrimeSpectrum` `Localization` `CommSemiring.toCommMonoid` `Ideal.primeCompl` `asIdeal` `isPrime` `OreLocalization.instSemiring` `OreLocalization.oreSetComm` `RingHom.instFunLike` `toPiLocalization`	—	`isPrime` `MaximalSpectrum.toPiLocalization_not_surjective_of_infinite` `piLocalizationToMaximal_comp_toPiLocalization` `piLocalizationToMaximal_surjective`

---

← Back to Index