Module

OpenImmersionQuotient.lean

Nyll.SchemeTheory.Morphisms.OpenImmersionQuotient

5 declarations indexed from sourceView source ↗

Module documentation

Open immersions after quotient base change

The literal map R / I → S / I S is the base change of a ring map R → S. Its pushout square is obtained from the tensor-product pushout and the canonical quotient/tensor-product equivalence. Consequently its spectrum is an open immersion whenever the original spectrum map is.

Imports7

Nyll.SchemeTheory.RingTheory.QuotientBaseChange
Mathlib.Algebra.Category.Ring.Constructions
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.CategoryTheory.MorphismProperty.Limits
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.TensorProduct.Quotient

Imported by2

theorem

isPushout_quotientMap

L37 ↗

CommRingCat.isPushout_quotientMap

Documentation

Extension of an ideal gives the canonical pushout square of quotient ring maps.

Source context 5 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u v
namespace CommRingCat

Lean source · statement

theorem isPushout_quotientMap {R S : Type u} [CommRing R] [CommRing S]
    (f : R →+* S) (I : Ideal R) :
    IsPushout (ofHom f) (ofHom (Ideal.Quotient.mk I))
      (ofHom (Ideal.Quotient.mk (I.map f)))
      (ofHom (Ideal.quotientMap (I.map f) f Ideal.le_comap_map))

theorem

isPullback_SpecMap_quotientMap

L64 ↗

AlgebraicGeometry.isPullback_SpecMap_quotientMap

Documentation

The canonical quotient square becomes a pullback square on spectra.

Source context 5 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry

Lean source · statement

theorem isPullback_SpecMap_quotientMap {R S : Type u} [CommRing R] [CommRing S]
    (f : R →+* S) (I : Ideal R) :
    IsPullback (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.map f))))
      (Spec.map (CommRingCat.ofHom
        (Ideal.quotientMap (I.map f) f Ideal.le_comap_map)))
      (Spec.map (CommRingCat.ofHom f))
      (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))

theorem

isOpenImmersion_SpecMap_quotientMap

L74 ↗

AlgebraicGeometry.isOpenImmersion_SpecMap_quotientMap

Documentation

Open immersions remain open immersions under the literal quotient map.

Source context 5 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry

Lean source · statement

theorem isOpenImmersion_SpecMap_quotientMap {R S : Type u} [CommRing R] [CommRing S]
    (f : R →+* S) (I : Ideal R)
    [IsOpenImmersion (Spec.map (CommRingCat.ofHom f))] :
    IsOpenImmersion (Spec.map (CommRingCat.ofHom
      (Ideal.quotientMap (I.map f) f Ideal.le_comap_map)))

theorem

isOpenImmersion_SpecMap_quotientMap_of_map_eq

L83 ↗

AlgebraicGeometry.isOpenImmersion_SpecMap_quotientMap_of_map_eq

Documentation

The same result with the extended ideal written using a chosen equal ideal.

Source context 5 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry

Lean source · statement

theorem isOpenImmersion_SpecMap_quotientMap_of_map_eq
    {R S : Type u} [CommRing R] [CommRing S]
    (f : R →+* S) (I : Ideal R) (J : Ideal S) (hJ : I.map f = J)
    [IsOpenImmersion (Spec.map (CommRingCat.ofHom f))] :
    IsOpenImmersion (Spec.map (CommRingCat.ofHom
      (Ideal.quotientMap J f (hJ ▸ Ideal.le_comap_map))))

theorem

isOpenImmersion_SpecMap_quotientBaseChange

L94 ↗

AlgebraicGeometry.isOpenImmersion_SpecMap_quotientBaseChange

Documentation

Reduction by an ideal in a common scalar ring preserves an open immersion for the canonical quotient-base algebra map.

Source context 5 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry

Lean source · statement

theorem isOpenImmersion_SpecMap_quotientBaseChange
    {R : Type v} {A B : Type u} [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (I : Ideal R)
    [IsOpenImmersion (Spec.map (CommRingCat.ofHom f.toRingHom))] :
    IsOpenImmersion (Spec.map (CommRingCat.ofHom (f.quotientBaseChange I).toRingHom))

Module documentation

Open immersions after quotient base change

Declarations

isPushout_quotientMap

isPullback_SpecMap_quotientMap

isOpenImmersion_SpecMap_quotientMap

isOpenImmersion_SpecMap_quotientMap_of_map_eq

isOpenImmersion_SpecMap_quotientBaseChange