ModuleIsNoetherianRing_exists_completeOrthogonalIdempotents_forall_connectedSpace_primeSpectrum.lean
Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsNoetherianRing_exists_completeOrthogonalIdempotents_forall_connectedSpace_primeSpectrum
3 declarations indexed from sourceView source ↗ Module documentation
Is Noetherian Ring exists complete Orthogonal Idempotents forall connected Space prime
Spectrum
Imports4
- Mathlib.RingTheory.Ideal.BigOperators
- Mathlib.RingTheory.Idempotents
- Mathlib.RingTheory.Spectrum.Prime.Noetherian
- Mathlib.Tactic.Choose
Imported by2
Declarations
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsNoetherianRing_exists_completeOrthogonalIdempotents_forall_connectedSpace_primeSpectrum.IdemDecompAux.finite_connectedComponents
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsNoetherianRing_exists_completeOrthogonalIdempotents_forall_connectedSpace_primeSpectrum
universe u
open TopologicalSpace PrimeSpectrum Topology
namespace IdemDecompAux
variable {X : Type*} [TopologicalSpace X]
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsNoetherianRing_exists_completeOrthogonalIdempotents_forall_connectedSpace_primeSpectrum.IdemDecompAux.isClopen_connectedComponent
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsNoetherianRing_exists_completeOrthogonalIdempotents_forall_connectedSpace_primeSpectrum
universe u
open TopologicalSpace PrimeSpectrum Topology
namespace IdemDecompAux
variable {X : Type*} [TopologicalSpace X]
IsNoetherianRing.exists_completeOrthogonalIdempotents_forall_connectedSpace_primeSpectrum
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsNoetherianRing_exists_completeOrthogonalIdempotents_forall_connectedSpace_primeSpectrum
universe u
open TopologicalSpace PrimeSpectrum Topology
open IdemDecompAux