Module

ProperLocalScalarSections.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.ProperLocalScalarSections

1 declaration indexed from sourceView source ↗

Module documentation

Scalar sections after arbitrary base change

For a proper flat finitely presented geometrically reduced family over any local ring, an isomorphism on the actual global-section map persists after arbitrary base change. This uses the proved section-algebra comparison and the actual tensor-product scalar inclusion, including nonflat residue-field changes.

Imports3

Nyll.EtaleFundamentalGroups.FiniteEtale.ProperLocalFiniteEtaleSections
Nyll.SchemeTheory.Cohomology.Cech.TwoAffineOpenCover
Mathlib.RingTheory.TensorProduct.Maps

Imported by2

theorem

isIso_appTop_baseChange_of_proper_flat_geometricallyReduced_local

L33 ↗

AlgebraicGeometry.isIso_appTop_baseChange_of_proper_flat_geometricallyReduced_local

Documentation

Scalar global sections persist after any coefficient change for a proper flat finitely presented geometrically reduced family over an arbitrary local ring.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicGeometry
universe u
open Scheme.TwoAffineOpenCover

Lean source · statement

theorem isIso_appTop_baseChange_of_proper_flat_geometricallyReduced_local
    {R : Type u} [CommRing R] [IsLocalRing R]
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R))
    [IsProper f] [Flat f] [LocallyOfFinitePresentation f]
    [GeometricallyReduced f] [IsIso f.appTop]
    (A : Type u) [CommRing A] [Algebra R A] :
    IsIso (pullback.snd f (specMap R A)).appTop

Module documentation

Scalar sections after arbitrary base change

Declarations

isIso_appTop_baseChange_of_proper_flat_geometricallyReduced_local