NYLL
Module

OpenImmersionLocalization.lean

Nyll.SchemeTheory.Morphisms.OpenImmersionLocalization
2 declarations indexed from sourceView source ↗

Module documentation

Localizing inside the image of an open immersion

An open immersion restricts to an isomorphism over any open contained in its image. For spectra, the canonical comparison with principal localization then proves bijectivity of the actual localized ring map. This applies to the principal neighborhood extracted from a normalization.

Imports6
  • Mathlib.AlgebraicGeometry.AffineScheme
  • Mathlib.AlgebraicGeometry.Morphisms.IsIso
  • Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
  • Mathlib.AlgebraicGeometry.Restrict
  • Mathlib.CategoryTheory.ConcreteCategory.EpiMono
  • Mathlib.CategoryTheory.MorphismProperty.Basic
Imported by2

Declarations

theorem

isIso_morphismRestrict_of_le_opensRange

L34 ↗
AlgebraicGeometry.Scheme.Hom.isIso_morphismRestrict_of_le_opensRange
Documentation

An open immersion is an isomorphism over every open contained in its image.

Source context 4 commands

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

@[expose] public section
open CategoryTheory
universe u
namespace AlgebraicGeometry
Lean source · statement
theorem Scheme.Hom.isIso_morphismRestrict_of_le_opensRange
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f]
    (U : Y.Opens) (hU : U ≤ f.opensRange) : IsIso (f ∣_ U)
theorem

bijective_awayMap_of_basicOpen_le_opensRange

L51 ↗
AlgebraicGeometry.bijective_awayMap_of_basicOpen_le_opensRange
Documentation

If D(r) lies in the image of an open immersion of spectra, localization at r makes the original ring map bijective.

Source context 4 commands

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

@[expose] public section
open CategoryTheory
universe u
namespace AlgebraicGeometry
Lean source · statement
theorem bijective_awayMap_of_basicOpen_le_opensRange
    {R S : CommRingCat.{u}} (f : R ⟶ S) [IsOpenImmersion (Spec.map f)]
    (r : R) (hr : PrimeSpectrum.basicOpen r ≤ (Spec.map f).opensRange) :
    Function.Bijective (Localization.awayMap f.hom r)

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