Nyll.SchemeTheory.RingTheory.TensorProductPrime

Module documentation

Compatible prime ideals lift to a tensor product

Two prime ideals of algebras over the same ring lift simultaneously to the tensor product when their contractions agree. The point is constructed in the scheme fiber product and transported through its affine tensor-product isomorphism, with both projections verified.

theorem

exists_tensorProduct_of_comap_eq

L28 ↗

PrimeSpectrum.exists_tensorProduct_of_comap_eq

Documentation

Compatible prime ideals lift to a prime of the tensor product, with both contractions prescribed. No dominance or flatness assumption is required.

Source context 4 commands

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

open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace PrimeSpectrum
universe u

Lean source · statement

theorem exists_tensorProduct_of_comap_eq
    (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
    [Algebra R B] [Algebra R C]
    (p : PrimeSpectrum B) (q : PrimeSpectrum C)
    (h : comap (algebraMap R B) p = comap (algebraMap R C) q) :
    ∃ r : PrimeSpectrum (B ⊗[R] C),
      comap (algebraMap B (B ⊗[R] C)) r = p ∧
        comap (Algebra.TensorProduct.includeRight (R := R) (A := B)).toRingHom r = q

Module documentation

Compatible prime ideals lift to a tensor product

Declarations

exists_tensorProduct_of_comap_eq