Module

isOpen_irreducibleComponent_of_isDomain_stalk.lean

Nyll.AlgebraicCurves.Geometry.Schemes.isOpen_irreducibleComponent_of_isDomain_stalk

4 declarations indexed from sourceView source ↗

Module documentation

is Open irreducible Component of is Domain stalk

Imports10

Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Noetherian
Mathlib.AlgebraicGeometry.Properties
Mathlib.AlgebraicGeometry.Stalk
Mathlib.RingTheory.Spectrum.Prime.Noetherian
Mathlib.Tactic.Set
Mathlib.Topology.Inseparable
Mathlib.Topology.Irreducible
Mathlib.Topology.NoetherianSpace
Mathlib.Topology.Sober

Imported by3

theorem

eq_irreducibleComponent_of_mem

L40 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isOpen_irreducibleComponent_of_isDomain_stalk.FltWs29.C2.eq_irreducibleComponent_of_mem

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.isOpen_irreducibleComponent_of_isDomain_stalk
universe u
open CategoryTheory AlgebraicGeometry
namespace FltWs29
namespace C2
open CategoryTheory AlgebraicGeometry TopologicalSpace Topology

Lean source · statement

theorem eq_irreducibleComponent_of_mem {X : Scheme.{u}} {x : X} (hx : IsDomain (X.presheaf.stalk x))
    {Z : Set X} (hZ : Z ∈ irreducibleComponents X) (hxZ : x ∈ Z) : Z = irreducibleComponent x

theorem

exists_open_subset_irreducibleComponent

L64 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isOpen_irreducibleComponent_of_isDomain_stalk.FltWs29.C2.exists_open_subset_irreducibleComponent

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.isOpen_irreducibleComponent_of_isDomain_stalk
universe u
open CategoryTheory AlgebraicGeometry
namespace FltWs29
namespace C2
open CategoryTheory AlgebraicGeometry TopologicalSpace Topology

Lean source · statement

theorem exists_open_subset_irreducibleComponent {X : Scheme.{u}} [IsLocallyNoetherian X]
    (hX : ∀ x : X, IsDomain (X.presheaf.stalk x)) (z : X) :
    ∃ O : Set X, IsOpen O ∧ z ∈ O ∧ O ⊆ irreducibleComponent z

theorem

main

L106 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isOpen_irreducibleComponent_of_isDomain_stalk.FltWs29.C2.main

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.isOpen_irreducibleComponent_of_isDomain_stalk
universe u
open CategoryTheory AlgebraicGeometry
namespace FltWs29
namespace C2
open CategoryTheory AlgebraicGeometry TopologicalSpace Topology

Lean source · statement

theorem main {X : Scheme.{u}} [IsLocallyNoetherian X] (hX : ∀ x : X, IsDomain (X.presheaf.stalk x))
  (x : X) :
    IsOpen (irreducibleComponent x) ∧ ∀ Z ∈ irreducibleComponents X, x ∈ Z → Z =
      irreducibleComponent x

theorem

isOpen_irreducibleComponent_of_isDomain_stalk

L120 ↗

AlgebraicGeometry.isOpen_irreducibleComponent_of_isDomain_stalk

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.isOpen_irreducibleComponent_of_isDomain_stalk
universe u
open CategoryTheory AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.isOpen_irreducibleComponent_of_isDomain_stalk
    {X : Scheme.{u}} [IsLocallyNoetherian X] (hX : ∀ x : X, IsDomain (X.presheaf.stalk x)) (x : X) :
    IsOpen (irreducibleComponent x) ∧ ∀ Z ∈ irreducibleComponents X, x ∈ Z → Z =
      irreducibleComponent x

Module documentation

is Open irreducible Component of is Domain stalk

Declarations

eq_irreducibleComponent_of_mem

exists_open_subset_irreducibleComponent

main

isOpen_irreducibleComponent_of_isDomain_stalk