The base change of a closed embedding

In the proof of [Kol07, Theorem 36], the change of fields for the resolution functor follows from that of the principalization functor, since an embedding i : X ↪ A over K and σ : K ↪ L give "another embedding i_{σ,L} : X_{σ,L} ↪ A_{σ,L}": a closed embedding over k base-changes to a closed embedding over L, with the base-changed ideal. This module proves it in the pullback-square form of IsBaseChangeOf (two cartesian squares over the same q : S' ⟶ S):

• baseChangeEmbedding emb hemb hX hA : X' ⟶ A', the morphism induced on the base changes by emb : X ⟶ A over S; baseChangeEmbedding_comp (⋯ ≫ pA = pX ≫ emb) and baseChangeEmbedding_over (⋯ ≫ fA' = fX');
• isPullback_baseChangeEmbedding: the square X' → A', X → A over pX, pA is a pullback (pasting, IsPullback.of_right);
• isClosedImmersion_baseChangeEmbedding: a closed immersion base-changes to a closed immersion;
• ker_baseChangeEmbedding: its kernel is the inverse image emb.ker.comap pA of the kernel (ker_fst_of_isClosedImmersion on the canonical pullback);
• baseChangeEmbedding_eq_pullback_map: on the canonical pullbacks it is pullback.map.

noncomputable def AlgebraicGeometry.baseChangeEmbedding {X A S X' A' S' : Scheme} (emb : X ⟶ A) {fX : X ⟶ S} {fA : A ⟶ S} (hemb : CategoryTheory.CategoryStruct.comp emb fA = fX) {q : S' ⟶ S} {pX : X' ⟶ X} {fX' : X' ⟶ S'} (hX : CategoryTheory.IsPullback pX fX' fX q) {pA : A' ⟶ A} {fA' : A' ⟶ S'} (hA : CategoryTheory.IsPullback pA fA' fA q) : X' ⟶ A'

The morphism induced on the base changes X' → X, A' → A (two pullback squares over q : S' → S) by a morphism emb : X ⟶ A over S: Kollár's i_{σ,L} : X_{σ,L} ↪ A_{σ,L} in the proof of [Kol07, Theorem 36].

Equations

• AlgebraicGeometry.baseChangeEmbedding emb hemb hX hA = hA.lift (CategoryTheory.CategoryStruct.comp pX emb) fX' ⋯

@[simp]

theorem AlgebraicGeometry.baseChangeEmbedding_comp {X A S X' A' S' : Scheme} (emb : X ⟶ A) {fX : X ⟶ S} {fA : A ⟶ S} (hemb : CategoryTheory.CategoryStruct.comp emb fA = fX) {q : S' ⟶ S} {pX : X' ⟶ X} {fX' : X' ⟶ S'} (hX : CategoryTheory.IsPullback pX fX' fX q) {pA : A' ⟶ A} {fA' : A' ⟶ S'} (hA : CategoryTheory.IsPullback pA fA' fA q) : CategoryTheory.CategoryStruct.comp (baseChangeEmbedding emb hemb hX hA) pA = CategoryTheory.CategoryStruct.comp pX emb

@[simp]

theorem AlgebraicGeometry.baseChangeEmbedding_comp_assoc {X A S X' A' S' : Scheme} (emb : X ⟶ A) {fX : X ⟶ S} {fA : A ⟶ S} (hemb : CategoryTheory.CategoryStruct.comp emb fA = fX) {q : S' ⟶ S} {pX : X' ⟶ X} {fX' : X' ⟶ S'} (hX : CategoryTheory.IsPullback pX fX' fX q) {pA : A' ⟶ A} {fA' : A' ⟶ S'} (hA : CategoryTheory.IsPullback pA fA' fA q) {Z : Scheme} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeEmbedding emb hemb hX hA) (CategoryTheory.CategoryStruct.comp pA h) = CategoryTheory.CategoryStruct.comp pX (CategoryTheory.CategoryStruct.comp emb h)

@[simp]

theorem AlgebraicGeometry.baseChangeEmbedding_over {X A S X' A' S' : Scheme} (emb : X ⟶ A) {fX : X ⟶ S} {fA : A ⟶ S} (hemb : CategoryTheory.CategoryStruct.comp emb fA = fX) {q : S' ⟶ S} {pX : X' ⟶ X} {fX' : X' ⟶ S'} (hX : CategoryTheory.IsPullback pX fX' fX q) {pA : A' ⟶ A} {fA' : A' ⟶ S'} (hA : CategoryTheory.IsPullback pA fA' fA q) : CategoryTheory.CategoryStruct.comp (baseChangeEmbedding emb hemb hX hA) fA' = fX'

@[simp]

theorem AlgebraicGeometry.baseChangeEmbedding_over_assoc {X A S X' A' S' : Scheme} (emb : X ⟶ A) {fX : X ⟶ S} {fA : A ⟶ S} (hemb : CategoryTheory.CategoryStruct.comp emb fA = fX) {q : S' ⟶ S} {pX : X' ⟶ X} {fX' : X' ⟶ S'} (hX : CategoryTheory.IsPullback pX fX' fX q) {pA : A' ⟶ A} {fA' : A' ⟶ S'} (hA : CategoryTheory.IsPullback pA fA' fA q) {Z : Scheme} (h : S' ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeEmbedding emb hemb hX hA) (CategoryTheory.CategoryStruct.comp fA' h) = CategoryTheory.CategoryStruct.comp fX' h

theorem AlgebraicGeometry.isPullback_baseChangeEmbedding {X A S X' A' S' : Scheme} (emb : X ⟶ A) {fX : X ⟶ S} {fA : A ⟶ S} (hemb : CategoryTheory.CategoryStruct.comp emb fA = fX) {q : S' ⟶ S} {pX : X' ⟶ X} {fX' : X' ⟶ S'} (hX : CategoryTheory.IsPullback pX fX' fX q) {pA : A' ⟶ A} {fA' : A' ⟶ S'} (hA : CategoryTheory.IsPullback pA fA' fA q) : CategoryTheory.IsPullback (baseChangeEmbedding emb hemb hX hA) pX pA emb

The base change of emb is a pullback square over pA, pX (pasting with the square of A).

theorem AlgebraicGeometry.isClosedImmersion_baseChangeEmbedding {X A S X' A' S' : Scheme} (emb : X ⟶ A) {fX : X ⟶ S} {fA : A ⟶ S} (hemb : CategoryTheory.CategoryStruct.comp emb fA = fX) {q : S' ⟶ S} {pX : X' ⟶ X} {fX' : X' ⟶ S'} (hX : CategoryTheory.IsPullback pX fX' fX q) {pA : A' ⟶ A} {fA' : A' ⟶ S'} (hA : CategoryTheory.IsPullback pA fA' fA q) [IsClosedImmersion emb] : IsClosedImmersion (baseChangeEmbedding emb hemb hX hA)

A closed immersion base-changes to a closed immersion.

theorem AlgebraicGeometry.ker_baseChangeEmbedding {X A S X' A' S' : Scheme} (emb : X ⟶ A) {fX : X ⟶ S} {fA : A ⟶ S} (hemb : CategoryTheory.CategoryStruct.comp emb fA = fX) {q : S' ⟶ S} {pX : X' ⟶ X} {fX' : X' ⟶ S'} (hX : CategoryTheory.IsPullback pX fX' fX q) {pA : A' ⟶ A} {fA' : A' ⟶ S'} (hA : CategoryTheory.IsPullback pA fA' fA q) [IsClosedImmersion emb] : Scheme.Hom.ker (baseChangeEmbedding emb hemb hX hA) = (Scheme.Hom.ker emb).comap pA

The kernel of the base-changed embedding is the inverse image of the kernel, I_{X_L} = p^* I_X (the proof of [Kol07, Theorem 36]).

theorem AlgebraicGeometry.baseChangeEmbedding_eq_pullback_map {X A S S' : Scheme} (emb : X ⟶ A) (fX : X ⟶ S) (fA : A ⟶ S) (hemb : CategoryTheory.CategoryStruct.comp emb fA = fX) (q : S' ⟶ S) : baseChangeEmbedding emb hemb ⋯ ⋯ = CategoryTheory.Limits.pullback.map fX q fA q emb (CategoryTheory.CategoryStruct.id S') (CategoryTheory.CategoryStruct.id S) ⋯ ⋯

On the canonical pullbacks X ×_S S', A ×_S S', the induced morphism is pullback.map.