AlgebraicGeometry.finitePresentation_sectionAlgebra_of_proper_flat_geometricallyReduced
Global sections are finitely presented over the original affine base, by descent to a proper flat Noetherian model and actual section base change.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicGeometry
universe uLean source · full declaration
theorem finitePresentation_sectionAlgebra_of_proper_flat_geometricallyReduced
{R : Type u} [CommRing R] {X : Scheme.{u}}
(f : X ⟶ Spec (CommRingCat.of R)) [IsProper f] [Flat f]
[LocallyOfFinitePresentation f] [GeometricallyReduced f] :
let : Algebra R Γ(X, ⊤) :=
((Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ f.appTop).hom.toAlgebra
Module.FinitePresentation R Γ(X, ⊤) := by
intro hRΓ
let : Algebra (ULift.{u} ℤ) R :=
((algebraMap ℤ R).comp (ULift.ringEquiv (R := ℤ)).toRingHom).toAlgebra
have hIntegers : IsNoetherianRing (ULift.{u} ℤ) :=
isNoetherianRing_of_ringEquiv ℤ (ULift.ringEquiv (R := ℤ)).symm
obtain ⟨S, hS, _, Y, g, p, hProper, hFlat, hModel⟩ :=
ProperFlatFinitePresentationDescent (A₀ := ULift.{u} ℤ) f ∅
have hFiniteTypeS : Algebra.FiniteType (ULift.{u} ℤ) S :=
(Subalgebra.fg_iff_finiteType S).mp hS
have hNoetherianS : IsNoetherianRing S :=
Algebra.FiniteType.isNoetherianRing (ULift.{u} ℤ) S
let hSΓ : Algebra S Γ(Y, ⊤) :=
((Scheme.ΓSpecIso (CommRingCat.of S)).inv ≫ g.appTop).hom.toAlgebra
have hfin : Module.Finite S Γ(Y, ⊤) :=
(finite_appTop_of_isProper_of_isNoetherianRing g).comp
(RingHom.Finite.of_surjective _
(Scheme.ΓSpecIso (CommRingCat.of S)).commRingCatIsoToRingEquiv.symm.surjective)
have hfp : Module.FinitePresentation S Γ(Y, ⊤) :=
Module.finitePresentation_of_finite S Γ(Y, ⊤)
have hSections := isPushout_sections_of_proper_flat_noetherian_model g f p hModel
let eRing := (CommRingCat.isPushout_tensorProduct S R Γ(Y, ⊤)).isoPushout ≪≫
hSections.isoPushout.symm
let e : R ⊗[S] Γ(Y, ⊤) ≃ₐ[R] Γ(X, ⊤) := {
toRingEquiv := eRing.commRingCatIsoToRingEquiv
commutes' := fun r => by
change (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom ≫ eRing.hom) r =
((Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ f.appTop) r
congr 2
simp only [eRing, Iso.trans_hom, Iso.symm_hom,
IsPushout.inl_isoPushout_hom_assoc, IsPushout.inl_isoPushout_inv] }
exact Module.FinitePresentation.of_equiv e.toLinearEquiv