Module

SpecFlatBaseChangeSections.lean

Nyll.SchemeTheory.Affine.SpecFlatBaseChangeSections

3 declarations indexed from sourceView source ↗

Module documentation

Flat base change on sections with the original affine coefficient rings

The scalar maps here are the actual maps from the rings defining the two affine bases. This comparison is used for residue-field coefficients in proper-family cohomology, where the original field actions must agree.

Imports2

Nyll.SchemeTheory.Affine.FlatBaseChangeAffinization
Mathlib.Algebra.Category.Ring.Constructions

Imported by6

theorem

isPushout_specPullbackSections

L33 ↗

AlgebraicGeometry.isPushout_specPullbackSections

Documentation

Flat base change on global sections as a pushout with the given base rings, and with the actual scalar and pullback maps.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicGeometry
universe u
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
variable [Module.Flat R A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R))
variable [QuasiCompact f] [QuasiSeparated f]

Lean source · statement

theorem isPushout_specPullbackSections :
    IsPushout (CommRingCat.ofHom (algebraMap R A))
      ((Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ f.appTop)
      ((Scheme.ΓSpecIso (CommRingCat.of A)).inv ≫
        (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap R A)))).appTop)
      (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap R A)))).appTop

def

specPullbackSectionsTensorEquiv

L53 ↗

AlgebraicGeometry.specPullbackSectionsTensorEquiv

Documentation

The global-section tensor comparison retains the original affine base ring as scalar owner.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicGeometry
universe u
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
variable [Module.Flat R A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R))
variable [QuasiCompact f] [QuasiSeparated f]

Lean source · full declaration

def specPullbackSectionsTensorEquiv :
    let : Algebra R Γ(X, ⊤) :=
      ((Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ f.appTop).hom.toAlgebra
    let : Algebra A Γ(pullback f
        (Spec.map (CommRingCat.ofHom (algebraMap R A))), ⊤) :=
      ((Scheme.ΓSpecIso (CommRingCat.of A)).inv ≫
        (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap R A)))).appTop).hom.toAlgebra
    A ⊗[R] Γ(X, ⊤) ≃ₐ[A]
      Γ(pullback f (Spec.map (CommRingCat.ofHom (algebraMap R A))), ⊤) := by
  intro hRX hAP
  let e := (CommRingCat.isPushout_tensorProduct R A Γ(X, ⊤)).isoPushout ≪≫
    (isPushout_specPullbackSections (A := A) f).isoPushout.symm
  refine { toRingEquiv := e.commRingCatIsoToRingEquiv, commutes' := ?_ }
  intro a
  change (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom ≫ e.hom) a =
    ((Scheme.ΓSpecIso (CommRingCat.of A)).inv ≫
      (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap R A)))).appTop) a
  congr 2
  simp only [e, Iso.trans_hom, Iso.symm_hom,
    IsPushout.inl_isoPushout_hom_assoc, IsPushout.inl_isoPushout_inv]

theorem

specPullbackSectionsTensorEquiv_one_tmul

L76 ↗

AlgebraicGeometry.specPullbackSectionsTensorEquiv_one_tmul

Documentation

The tensor comparison sends the right factor to the actual restriction from the source scheme.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicGeometry
universe u
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
variable [Module.Flat R A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R))
variable [QuasiCompact f] [QuasiSeparated f]

Lean source · full declaration

theorem specPullbackSectionsTensorEquiv_one_tmul :
    let : Algebra R Γ(X, ⊤) :=
      ((Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ f.appTop).hom.toAlgebra
    let : Algebra A Γ(pullback f
        (Spec.map (CommRingCat.ofHom (algebraMap R A))), ⊤) :=
      ((Scheme.ΓSpecIso (CommRingCat.of A)).inv ≫
        (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap R A)))).appTop).hom.toAlgebra
    ∀ x : Γ(X, ⊤), specPullbackSectionsTensorEquiv (A := A) f (1 ⊗ₜ[R] x) =
      (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap R A)))).appTop x := by
  intro hRX hAP x
  change (CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom ≫
    ((CommRingCat.isPushout_tensorProduct R A Γ(X, ⊤)).isoPushout ≪≫
      (isPushout_specPullbackSections (A := A) f).isoPushout.symm).hom) x = _
  congr 2
  simp only [Iso.trans_hom, Iso.symm_hom,
    IsPushout.inr_isoPushout_hom_assoc, IsPushout.inr_isoPushout_inv]

Module documentation

Flat base change on sections with the original affine coefficient rings

Declarations

isPushout_specPullbackSections

specPullbackSectionsTensorEquiv

specPullbackSectionsTensorEquiv_one_tmul