NYLL
Module

isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk.lean

Nyll.AlgebraicCurves.Geometry.Schemes.isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk
14 declarations indexed from sourceView source ↗

Module documentation

is Integral of is Locally Noetherian of connected Space of forall is Domain stalk

Imports1
  • Mathlib.AlgebraicGeometry.Noetherian
Imported by6

Declarations

theorem

isPreirreducible_union_of_isOpen_of_mem

L34 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk.N3da397ad0.isPreirreducible_union_of_isOpen_of_mem
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk
universe u
open CategoryTheory AlgebraicGeometry
namespace N3da397ad0
section Topology
variable {α : Type*} [TopologicalSpace α]
Lean source · statement
theorem isPreirreducible_union_of_isOpen_of_mem {s U : Set α}
    (hs : IsPreirreducible s) (hU : IsPreirreducible U) (hUopen : IsOpen U)
    {y : α} (hys : y ∈ s) (hyU : y ∈ U) : IsPreirreducible (s ∪ U)
theorem

isOpen_irreducibleComponent_of_forall_isPreirreducible_nhd

L47 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk.N3da397ad0.isOpen_irreducibleComponent_of_forall_isPreirreducible_nhd
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk
universe u
open CategoryTheory AlgebraicGeometry
namespace N3da397ad0
section Topology
variable {α : Type*} [TopologicalSpace α]
Lean source · statement
theorem isOpen_irreducibleComponent_of_forall_isPreirreducible_nhd
    (hloc : ∀ y : α, ∃ U : Set α, IsOpen U ∧ y ∈ U ∧ IsPreirreducible U) (x : α) :
    IsOpen (irreducibleComponent x)
theorem

connectedComponent_eq_irreducibleComponent_of_forall_isPreirreducible_nhd

L63 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk.N3da397ad0.connectedComponent_eq_irreducibleComponent_of_forall_isPreirreducible_nhd
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk
universe u
open CategoryTheory AlgebraicGeometry
namespace N3da397ad0
section Topology
variable {α : Type*} [TopologicalSpace α]
Lean source · statement
theorem connectedComponent_eq_irreducibleComponent_of_forall_isPreirreducible_nhd
    (hloc : ∀ y : α, ∃ U : Set α, IsOpen U ∧ y ∈ U ∧ IsPreirreducible U) (x : α) :
    connectedComponent x = irreducibleComponent x
theorem

isPreirreducible_connectedComponent_of_forall_isPreirreducible_nhd

L75 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk.N3da397ad0.isPreirreducible_connectedComponent_of_forall_isPreirreducible_nhd
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk
universe u
open CategoryTheory AlgebraicGeometry
namespace N3da397ad0
section Topology
variable {α : Type*} [TopologicalSpace α]
Lean source · statement
theorem isPreirreducible_connectedComponent_of_forall_isPreirreducible_nhd
    (hloc : ∀ y : α, ∃ U : Set α, IsOpen U ∧ y ∈ U ∧ IsPreirreducible U) (x : α) :
    IsPreirreducible (connectedComponent x)
theorem

eq_of_mem_minimalPrimes_of_le_of_isDomain_localizationAtPrime

L87 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk.N3da397ad0.eq_of_mem_minimalPrimes_of_le_of_isDomain_localizationAtPrime
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk
universe u
open CategoryTheory AlgebraicGeometry
namespace N3da397ad0
section Ring
variable {R : Type u} [CommRing R]
Lean source · statement
theorem eq_of_mem_minimalPrimes_of_le_of_isDomain_localizationAtPrime
    {p : Ideal R} [hp : p.IsPrime] (hdom : IsDomain (Localization.AtPrime p))
    {q₁ q₂ : Ideal R} (h₁ : q₁ ∈ minimalPrimes R) (h₂ : q₂ ∈ minimalPrimes R)
    (hle₁ : q₁ ≤ p) (hle₂ : q₂ ≤ p) : q₁ = q₂
theorem

exists_mem_zeroLocus_minimalPrimes

L114 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk.N3da397ad0.exists_mem_zeroLocus_minimalPrimes
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk
universe u
open CategoryTheory AlgebraicGeometry
namespace N3da397ad0
section Ring
variable {R : Type u} [CommRing R]
Lean source · statement
theorem exists_mem_zeroLocus_minimalPrimes (x : PrimeSpectrum R) :
    ∃ q ∈ minimalPrimes R, x ∈ PrimeSpectrum.zeroLocus (q : Set R)
theorem

compl_zeroLocus_eq_biUnion

L120 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk.N3da397ad0.compl_zeroLocus_eq_biUnion
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk
universe u
open CategoryTheory AlgebraicGeometry
namespace N3da397ad0
section Ring
variable {R : Type u} [CommRing R]
Lean source · statement
theorem compl_zeroLocus_eq_biUnion
    (huniq : ∀ q₁ q₂ : Ideal R, q₁ ∈ minimalPrimes R → q₂ ∈ minimalPrimes R →
      ∀ p : Ideal R, p.IsPrime → q₁ ≤ p → q₂ ≤ p → q₁ = q₂)
    {q₀ : Ideal R} (hq₀ : q₀ ∈ minimalPrimes R) :
    (PrimeSpectrum.zeroLocus (q₀ : Set R))ᶜ
      = ⋃ q ∈ minimalPrimes R \ {q₀}, PrimeSpectrum.zeroLocus ((q : Ideal R) : Set R)
theorem

isClopen_zeroLocus_of_mem_minimalPrimes

L141 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk.N3da397ad0.isClopen_zeroLocus_of_mem_minimalPrimes
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk
universe u
open CategoryTheory AlgebraicGeometry
namespace N3da397ad0
section Ring
variable {R : Type u} [CommRing R]
Lean source · statement
theorem isClopen_zeroLocus_of_mem_minimalPrimes [IsNoetherianRing R]
    (huniq : ∀ q₁ q₂ : Ideal R, q₁ ∈ minimalPrimes R → q₂ ∈ minimalPrimes R →
      ∀ p : Ideal R, p.IsPrime → q₁ ≤ p → q₂ ≤ p → q₁ = q₂)
    {q₀ : Ideal R} (hq₀ : q₀ ∈ minimalPrimes R) :
    IsClopen (PrimeSpectrum.zeroLocus (q₀ : Set R))
theorem

exists_isClopen_isPreirreducible_mem_of_forall_isDomain_localizationAtPrime

L152 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk.N3da397ad0.exists_isClopen_isPreirreducible_mem_of_forall_isDomain_localizationAtPrime
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk
universe u
open CategoryTheory AlgebraicGeometry
namespace N3da397ad0
section Ring
variable {R : Type u} [CommRing R]
Lean source · statement
theorem exists_isClopen_isPreirreducible_mem_of_forall_isDomain_localizationAtPrime
    [IsNoetherianRing R]
    (hstalk : ∀ (p : Ideal R) [p.IsPrime], IsDomain (Localization.AtPrime p))
    (x : PrimeSpectrum R) :
    ∃ s : Set (PrimeSpectrum R), IsClopen s ∧ x ∈ s ∧ IsPreirreducible s
theorem

isDomain_localizationAtPrime_of_isLocalization

L175 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk.N3da397ad0.isDomain_localizationAtPrime_of_isLocalization
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk
universe u
open CategoryTheory AlgebraicGeometry
namespace N3da397ad0
section SchemeTransport
Lean source · statement
theorem isDomain_localizationAtPrime_of_isLocalization {R : Type u} [CommRing R]
    (p : Ideal R) [p.IsPrime] (S : Type u) [CommRing S] [Algebra R S]
    [IsLocalization p.primeCompl S] [IsDomain S] :
    IsDomain (Localization.AtPrime p)
theorem

exists_primeIdealOf_eq

L182 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk.N3da397ad0.exists_primeIdealOf_eq
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk
universe u
open CategoryTheory AlgebraicGeometry
namespace N3da397ad0
section SchemeTransport
Lean source · statement
theorem exists_primeIdealOf_eq {X : Scheme.{u}} {U : X.Opens}
    (hU : IsAffineOpen U) (p : PrimeSpectrum Γ(X, U)) :
    ∃ y : ↥U, hU.primeIdealOf y = p
theorem

exists_isOpen_mem_isPreirreducible_of_forall_isDomain_stalk

L190 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk.N3da397ad0.exists_isOpen_mem_isPreirreducible_of_forall_isDomain_stalk
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk
universe u
open CategoryTheory AlgebraicGeometry
namespace N3da397ad0
section SchemeTransport
Lean source · statement
theorem exists_isOpen_mem_isPreirreducible_of_forall_isDomain_stalk
    (X : Scheme.{u}) [IsLocallyNoetherian X]
    (hstalk : ∀ x : ↥X, IsDomain (X.presheaf.stalk x)) (x : ↥X) :
    ∃ s : Set ↥X, IsOpen s ∧ x ∈ s ∧ IsPreirreducible s
theorem

isPreirreducible_connectedComponent_of_forall_isDomain_stalk

L216 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk.N3da397ad0.isPreirreducible_connectedComponent_of_forall_isDomain_stalk
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk
universe u
open CategoryTheory AlgebraicGeometry
namespace N3da397ad0
section SchemeTransport
Lean source · statement
theorem isPreirreducible_connectedComponent_of_forall_isDomain_stalk
    (T : Scheme.{u}) [IsLocallyNoetherian T]
    (hstalk : ∀ x : ↥T, IsDomain (T.presheaf.stalk x)) (x : ↥T) :
    IsPreirreducible (connectedComponent x)
theorem

isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk

L236 ↗
AlgebraicGeometry.isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicGeometry
universe u
open CategoryTheory
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk in
Lean source · statement
theorem isIntegral_of_isLocallyNoetherian_of_connectedSpace_of_forall_isDomain_stalk
    (X : Scheme.{u}) [IsLocallyNoetherian X] [ConnectedSpace X]
    (h : ∀ x : X, IsDomain (X.presheaf.stalk x)) : IsIntegral X

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.