Module

exists_isAffineOpen_forall_mem_of_isImmersion_proj.lean

Nyll.AlgebraicCurves.Geometry.Schemes.exists_isAffineOpen_forall_mem_of_isImmersion_proj

5 declarations indexed from sourceView source ↗

Module documentation

exists is Affine Open forall mem of is Immersion proj

Imports3

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Mathlib.AlgebraicGeometry.Morphisms.Immersion
Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HomogeneousIdeal_exists_homogeneous_pos_mem_forall_notMem

Imported by2

theorem

exists_basicOpen_le_forall_mem_of_finset

L42 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isAffineOpen_forall_mem_of_isImmersion_proj.AlgebraicGeometry.Proj.exists_basicOpen_le_forall_mem_of_finset

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_isAffineOpen_forall_mem_of_isImmersion_proj
universe u v
open CategoryTheory
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section ProjOpen
variable {A σ : Type*} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜]
open scoped Proj in

Lean source · statement

theorem Proj.exists_basicOpen_le_forall_mem_of_finset (U : (Proj 𝒜).Opens) (S : Finset (Proj 𝒜))
    (hS : ∀ x ∈ S, x ∈ U) :
    ∃ (n : ℕ) (f : A), 0 < n ∧ f ∈ 𝒜 n ∧ Proj.basicOpen 𝒜 f ≤ U ∧ ∀ x ∈ S, x ∈ Proj.basicOpen 𝒜 f

theorem

exists_isAffineOpen_le_forall_mem_of_finset

L84 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isAffineOpen_forall_mem_of_isImmersion_proj.AlgebraicGeometry.Proj.exists_isAffineOpen_le_forall_mem_of_finset

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_isAffineOpen_forall_mem_of_isImmersion_proj
universe u v
open CategoryTheory
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section ProjOpen
variable {A σ : Type*} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜]
open scoped Proj in

Lean source · statement

theorem Proj.exists_isAffineOpen_le_forall_mem_of_finset (U : (Proj 𝒜).Opens) (S : Finset (Proj 𝒜))
    (hS : ∀ x ∈ S, x ∈ U) :
    ∃ V : (Proj 𝒜).Opens, IsAffineOpen V ∧ V ≤ U ∧ ∀ x ∈ S, x ∈ V

theorem

ι_preimage_of_le

L96 ↗

AlgebraicGeometry.IsAffineOpen.ι_preimage_of_le

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_isAffineOpen_forall_mem_of_isImmersion_proj
universe u v
open CategoryTheory
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace IsAffineOpen

Lean source · statement

theorem _root_.AlgebraicGeometry.IsAffineOpen.ι_preimage_of_le {Y : Scheme.{u}} {U V :
  Y.Opens} (hV : IsAffineOpen V) (h : V ≤ U) :
    IsAffineOpen (U.ι ⁻¹ᵁ V)

theorem

exists_isAffineOpen_forall_mem_of_isImmersion

L108 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isAffineOpen_forall_mem_of_isImmersion_proj.AlgebraicGeometry.exists_isAffineOpen_forall_mem_of_isImmersion

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_isAffineOpen_forall_mem_of_isImmersion_proj
universe u v
open CategoryTheory
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry

Lean source · statement

theorem exists_isAffineOpen_forall_mem_of_isImmersion {X Y : Scheme.{u}} (ι : X ⟶ Y) [IsImmersion ι]
    (hY : ∀ (U : Y.Opens) (T : Finset Y), (∀ y ∈ T, y ∈ U) →
      ∃ V : Y.Opens, IsAffineOpen V ∧ V ≤ U ∧ ∀ y ∈ T, y ∈ V)
    (S : Finset X) : ∃ W : X.Opens, IsAffineOpen W ∧ ∀ x ∈ S, x ∈ W

theorem

exists_isAffineOpen_forall_mem_of_isImmersion_proj

L128 ↗

AlgebraicGeometry.exists_isAffineOpen_forall_mem_of_isImmersion_proj

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_isAffineOpen_forall_mem_of_isImmersion_proj
universe u v
open CategoryTheory

Lean source · statement

theorem _root_.AlgebraicGeometry.exists_isAffineOpen_forall_mem_of_isImmersion_proj
    {A : Type u} {σ : Type v} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ)
      [GradedRing 𝒜]
    {X : AlgebraicGeometry.Scheme.{u}} (ι : X ⟶ AlgebraicGeometry.Proj 𝒜)
      [AlgebraicGeometry.IsImmersion ι]
    (S : Finset X) :
    ∃ W : X.Opens, AlgebraicGeometry.IsAffineOpen W ∧ ∀ x ∈ S, x ∈ W

Module documentation

exists is Affine Open forall mem of is Immersion proj

Declarations

exists_basicOpen_le_forall_mem_of_finset

exists_isAffineOpen_le_forall_mem_of_finset

ι_preimage_of_le

exists_isAffineOpen_forall_mem_of_isImmersion

exists_isAffineOpen_forall_mem_of_isImmersion_proj