Module

AffineComplement.lean

Nyll.SchemeTheory.Divisors.AffineComplement

6 declarations indexed from sourceView source ↗

Module documentation

Principal affine charts of a divisor complement

The generator of the ideal on an affine chart identifies the actual inverse image of the support complement with a principal open. The resulting map from the principal localization forms a pullback square with that complement.

Imports3

Nyll.SchemeTheory.Divisors.LocalComplement
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.Morphisms.Basic

Imported by2

theorem

fromSpec_mem_support_iff_of_ideal_eq_span

L35 ↗

AlgebraicGeometry.Scheme.IdealSheafData.fromSpec_mem_support_iff_of_ideal_eq_span

Documentation

Membership in the boundary on an affine principal chart is detected by the actual generator in its coordinate-ring prime.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X : Scheme.{u}} (I : X.IdealSheafData)
  {U : X.Opens} (hU : IsAffineOpen U) (d : Γ(X, U))
  (hd : I.ideal ⟨U, hU⟩ = Ideal.span {d})
include hd

Lean source · statement

theorem fromSpec_mem_support_iff_of_ideal_eq_span
    (p : PrimeSpectrum Γ(X, U)) : hU.fromSpec p ∈ I.support ↔ d ∈ p.asIdeal

theorem

fromSpec_preimage_supportComplement_of_ideal_eq_span

L49 ↗

AlgebraicGeometry.Scheme.IdealSheafData.fromSpec_preimage_supportComplement_of_ideal_eq_span

Documentation

The inverse image of a principal divisor complement is the matching basic open in the spectrum of the affine chart.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X : Scheme.{u}} (I : X.IdealSheafData)
  {U : X.Opens} (hU : IsAffineOpen U) (d : Γ(X, U))
  (hd : I.ideal ⟨U, hU⟩ = Ideal.span {d})
include hd

Lean source · statement

theorem fromSpec_preimage_supportComplement_of_ideal_eq_span :
    hU.fromSpec ⁻¹ᵁ I.supportComplement = PrimeSpectrum.basicOpen d

theorem

affineAway_range_subset_supportComplement

L55 ↗

AlgebraicGeometry.Scheme.IdealSheafData.affineAway_range_subset_supportComplement

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X : Scheme.{u}} (I : X.IdealSheafData)
  {U : X.Opens} (hU : IsAffineOpen U) (d : Γ(X, U))
  (hd : I.ideal ⟨U, hU⟩ = Ideal.span {d})
include hd

Lean source · statement

theorem affineAway_range_subset_supportComplement :
    Set.range (Spec.map (CommRingCat.ofHom
        (algebraMap Γ(X, U) (Localization.Away d))) ≫ hU.fromSpec) ⊆
      Set.range I.supportComplement.ι

def

affineAwayToSupportComplement

L70 ↗

AlgebraicGeometry.Scheme.IdealSheafData.affineAwayToSupportComplement

Documentation

The actual map from a principal affine localization into the original divisor complement.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X : Scheme.{u}} (I : X.IdealSheafData)
  {U : X.Opens} (hU : IsAffineOpen U) (d : Γ(X, U))
  (hd : I.ideal ⟨U, hU⟩ = Ideal.span {d})
include hd

Lean source · statement

def affineAwayToSupportComplement :
    Spec (.of (Localization.Away d)) ⟶ I.supportComplement

theorem

affineAwayToSupportComplement_comp_ι

L78 ↗

AlgebraicGeometry.Scheme.IdealSheafData.affineAwayToSupportComplement_comp_ι

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X : Scheme.{u}} (I : X.IdealSheafData)
  {U : X.Opens} (hU : IsAffineOpen U) (d : Γ(X, U))
  (hd : I.ideal ⟨U, hU⟩ = Ideal.span {d})
include hd

Lean source · statement

theorem affineAwayToSupportComplement_comp_ι :
    affineAwayToSupportComplement I hU d hd ≫ I.supportComplement.ι =
      Spec.map (CommRingCat.ofHom (algebraMap Γ(X, U) (Localization.Away d))) ≫
        hU.fromSpec

theorem

isPullback_affineAwayToSupportComplement

L86 ↗

AlgebraicGeometry.Scheme.IdealSheafData.isPullback_affineAwayToSupportComplement

Documentation

The principal affine localization is the pullback of the original complement, with its specified map rather than an arbitrary isomorphism.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X : Scheme.{u}} (I : X.IdealSheafData)
  {U : X.Opens} (hU : IsAffineOpen U) (d : Γ(X, U))
  (hd : I.ideal ⟨U, hU⟩ = Ideal.span {d})
include hd

Lean source · statement

theorem isPullback_affineAwayToSupportComplement :
    IsPullback (affineAwayToSupportComplement I hU d hd)
      (Spec.map (CommRingCat.ofHom (algebraMap Γ(X, U) (Localization.Away d))))
      I.supportComplement.ι hU.fromSpec

Module documentation

Principal affine charts of a divisor complement

Declarations

fromSpec_mem_support_iff_of_ideal_eq_span

fromSpec_preimage_supportComplement_of_ideal_eq_span

affineAway_range_subset_supportComplement

affineAwayToSupportComplement

affineAwayToSupportComplement_comp_ι

isPullback_affineAwayToSupportComplement