Documentation

TauCeti.AlgebraicGeometry.Pullback.SpecMap

Pullback of schemes along Spec.map #

Mathlib's CategoryTheory.Over.pullbackId and CategoryTheory.Over.pullbackComp compare the pullback functors on Over categories along an identity morphism and along a composite. This file reads those comparisons through Spec: Spec.map takes an identity ring map to an identity morphism of schemes and a composite f ≫ g to Spec.map g ≫ Spec.map f, so pullback along Spec.map (𝟙 R) is the identity functor on schemes over Spec R, and pullback along Spec.map (f ≫ g) is the composite of pullback along Spec.map f with pullback along Spec.map g.

These two comparisons mention neither affineness nor group objects: they are statements about arbitrary schemes over an affine base, and they are the underlying comparisons of the base-change functors on affine group schemes in TauCeti/AlgebraicGeometry/AffineGroupScheme/BaseChange/Basic.lean.

The same pullback along Spec.map of a ring map k → K carries affine charts: if Spec A is an open subscheme of X over Spec k, then Spec (A ⊗[k] K) is an open subscheme of the base change X ×_k Spec K, over Spec K.

Main declarations #

source
noncomputable def TauCeti.AlgebraicGeometry.Over.pullbackSpecMapId {R : CommRingCat} :
CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CategoryTheory.CategoryStruct.id R)) ≅ CategoryTheory.Functor.id (CategoryTheory.Over (AlgebraicGeometry.Spec R))

Pullback along Spec.map (𝟙 R) is the identity functor on schemes over Spec R.

Instances For
    source
    noncomputable def TauCeti.AlgebraicGeometry.Over.pullbackSpecMapComp {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) :
    CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CategoryTheory.CategoryStruct.comp f g)) ≅ (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map f)).comp (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map g))

    Pullback along Spec.map (f ≫ g) is pullback along Spec.map f followed by pullback along Spec.map g.

    Instances For
      source
      theorem TauCeti.AlgebraicGeometry.exists_isOpenImmersion_tensorProduct_of_isPullback {k A K : Type u} [CommRing k] [CommRing A] [CommRing K] [Algebra k A] [Algebra k K] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ AlgebraicGeometry.Spec ↧k} {φ : AlgebraicGeometry.Spec ↧A ⟶ X} [AlgebraicGeometry.IsOpenImmersion φ] (hφ : CategoryTheory.CategoryStruct.comp φ f = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k A))) {g : Y ⟶ X} {q : Y ⟶ AlgebraicGeometry.Spec ↧K} (H : CategoryTheory.IsPullback g q f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k K)))) :
      ∃ (ι : AlgebraicGeometry.Spec ↧(TensorProduct k A K) ⟶ Y), AlgebraicGeometry.IsOpenImmersion ι ∧ CategoryTheory.CategoryStruct.comp ι q = AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom)

      The base change of an affine chart is an affine chart of the base change. Let φ : Spec A ⟶ X be an open immersion of schemes over Spec k, and let Y = X ×_k Spec K be a base change of X. Then Spec (A ⊗[k] K) is an open subscheme of Y, over Spec K.

      source
      noncomputable def TauCeti.AlgebraicGeometry.pullbackSpecIsoOfAlgEquiv (R B T C : Type u) [CommRing R] [CommRing B] [CommRing T] [CommRing C] [Algebra R B] [Algebra R T] [Algebra T C] (e : TensorProduct R T B ≃ₐ[T] C) :
      CategoryTheory.Over.mk (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.algebraMap R B) (AlgebraicGeometry.Spec.algebraMap R T)) ≅ CategoryTheory.Over.mk (AlgebraicGeometry.Spec.algebraMap T C)

      An algebraic identification of a base-changed algebra induces an isomorphism over the new affine base. No finiteness or étaleness assumptions are needed for this transport.

      Instances For
        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.pullbackSpecIsoOfAlgEquiv_hom_left (R B T C : Type u) [CommRing R] [CommRing B] [CommRing T] [CommRing C] [Algebra R B] [Algebra R T] [Algebra T C] (e : TensorProduct R T B ≃ₐ[T] C) :
        CategoryTheory.Over.Hom.left (pullbackSpecIsoOfAlgEquiv R B T C e).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (AlgebraicGeometry.Spec.algebraMap R B) (AlgebraicGeometry.Spec.algebraMap R T)).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R T B).hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom e.symm.toRingEquiv.toRingHom)))

        The underlying map of the affine base-change isomorphism is the standard pullback comparison followed by the spectrum map of the inverse algebra equivalence.