Module

ProjSpace_topologicalKrullDim_le_of_isClosedImmersion.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_topologicalKrullDim_le_of_isClosedImmersion

6 declarations indexed from sourceView source ↗

Module documentation

Proj Space topological Krull Dim le of is Closed Immersion

Imports4

Mathlib.Topology.KrullDimension
Mathlib.RingTheory.KrullDimension.Polynomial
Mathlib.RingTheory.KrullDimension.Field
Nyll.SchemeTheory.ProjectiveSpace.Basic

Imported by2

theorem

topologicalKrullDim_le_of_iSup_eq_top

L38 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_topologicalKrullDim_le_of_isClosedImmersion.DIMPROJSOL.topologicalKrullDim_le_of_iSup_eq_top

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_topologicalKrullDim_le_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
namespace DIMPROJSOL
open TopologicalSpace Order

Lean source · statement

theorem topologicalKrullDim_le_of_iSup_eq_top {X : Type u} [TopologicalSpace X] {ι : Type*}
    (U : ι → Opens X) (hU : iSup U = ⊤) (N : WithBot ℕ∞)
    (hN : ∀ i, topologicalKrullDim (U i) ≤ N) : topologicalKrullDim X ≤ N

theorem

ringKrullDim_away_le

L62 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_topologicalKrullDim_le_of_isClosedImmersion.DIMPROJSOL.ringKrullDim_away_le

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_topologicalKrullDim_le_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
namespace DIMPROJSOL
open TopologicalSpace Order
variable (k : Type u) [Field k] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k

Lean source · statement

theorem ringKrullDim_away_le (i : Fin (n + 1)) :
    ringKrullDim (HomogeneousLocalization.Away 𝒜 (X i)) ≤ n

theorem

topologicalKrullDim_basicOpen_le

L82 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_topologicalKrullDim_le_of_isClosedImmersion.DIMPROJSOL.topologicalKrullDim_basicOpen_le

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_topologicalKrullDim_le_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
namespace DIMPROJSOL
open TopologicalSpace Order
variable (k : Type u) [Field k] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k

Lean source · statement

theorem topologicalKrullDim_basicOpen_le (i : Fin (n + 1)) :
    topologicalKrullDim (Proj.basicOpen 𝒜 (X i)) ≤ n

theorem

iSup_basicOpen_X

L91 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_topologicalKrullDim_le_of_isClosedImmersion.DIMPROJSOL.iSup_basicOpen_X

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_topologicalKrullDim_le_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
namespace DIMPROJSOL
open TopologicalSpace Order
variable (k : Type u) [Field k] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k

Lean source · statement

theorem iSup_basicOpen_X : (⨆ i : Fin (n + 1), Proj.basicOpen 𝒜 (X i)) = ⊤

theorem

topologicalKrullDim_proj_le

L98 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_topologicalKrullDim_le_of_isClosedImmersion.DIMPROJSOL.topologicalKrullDim_proj_le

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_topologicalKrullDim_le_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
namespace DIMPROJSOL
open TopologicalSpace Order
variable (k : Type u) [Field k] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k

Lean source · statement

theorem topologicalKrullDim_proj_le : topologicalKrullDim (Proj 𝒜) ≤ n

theorem

topologicalKrullDim_le_of_isClosedImmersion

L105 ↗

AlgebraicGeometry.ProjSpace.topologicalKrullDim_le_of_isClosedImmersion

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_topologicalKrullDim_le_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
open DIMPROJSOL in

Lean source · statement

theorem _root_.AlgebraicGeometry.ProjSpace.topologicalKrullDim_le_of_isClosedImmersion
    {k : Type u} [Field k] {n : ℕ} {Z : Scheme.{u}}
    (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsClosedImmersion ι] :
    topologicalKrullDim Z ≤ n

Module documentation

Proj Space topological Krull Dim le of is Closed Immersion

Declarations

topologicalKrullDim_le_of_iSup_eq_top

ringKrullDim_away_le

topologicalKrullDim_basicOpen_le

iSup_basicOpen_X

topologicalKrullDim_proj_le

topologicalKrullDim_le_of_isClosedImmersion