Sections of finite morphisms

For a finite morphism f : X ⟶ Spec R, the global sections Γ(X, ⊤) form a finite R-module. AlgebraicGeometry.Scheme.Hom.moduleFinite_appTop states this for an existing R-algebra structure compatible with the map of global sections. It transports Mathlib's Scheme.Hom.finite_appTop across the canonical isomorphism R ≅ Γ(Spec R, ⊤).

This finiteness is used to compute the rank of a finite morphism over a field as the dimension of its global sections.

If g : Y ⟶ S is moreover flat and locally of finite presentation (finite locally free), its sections Γ(Y, g⁻¹ U) over an affine open U of S form a projective Γ(S, U)-module (AlgebraicGeometry.Scheme.Hom.projective_app).

Finite, flat and locally finitely presented morphisms each respect isomorphisms (TauCeti.isFinite_respectsIso, TauCeti.flat_respectsIso and TauCeti.locallyOfFinitePresentation_respectsIso).

theorem AlgebraicGeometry.Scheme.Hom.moduleFinite_appTop {R : Type u} [CommRing R] {X : Scheme} (f : X ⟶ Spec ↧R) [IsFinite f] [Algebra R ↑(X.presheaf.obj (Opposite.op ⊤))] (hf : algebraMap R ↑(X.presheaf.obj (Opposite.op ⊤)) = CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (ΓSpecIso ↧R).inv (appTop f))) : Module.Finite R ↑(X.presheaf.obj (Opposite.op ⊤))

A finite morphism to the spectrum of a commutative ring has module-finite global sections, for any R-algebra structure on Γ(X, ⊤) given by the map of global sections.

theorem AlgebraicGeometry.Scheme.Hom.projective_app {Y S : Scheme} (g : Y ⟶ S) [IsFinite g] [Flat g] [LocallyOfFinitePresentation g] (U : ↑S.affineOpens) : Module.Projective ↑(S.presheaf.obj (Opposite.op ↑U)) ↑(Y.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map g.base).obj ↑U)))

The sections of a finite, flat, locally finitely presented morphism g : Y ⟶ S over an affine open U of S form a projective module over Γ(S, U).

instance TauCeti.isFinite_respectsIso : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.IsFinite

Finite morphisms of schemes respect isomorphisms.

instance TauCeti.flat_respectsIso : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.Flat

Flat morphisms of schemes respect isomorphisms.

instance TauCeti.locallyOfFinitePresentation_respectsIso : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.LocallyOfFinitePresentation

Morphisms of schemes locally of finite presentation respect isomorphisms.