NYLL
Module

ProperNoetherianModelSections.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.ProperNoetherianModelSections
5 declarations indexed from sourceView source ↗

Module documentation

Section comparisons for an actual Noetherian model

The closed-fibre comparison yields a pushout of the actual section maps. This form retains the maps needed to compare a Noetherian model with an arbitrary base and its localizations.

Imports7
Imported by2

Declarations

theorem

bijective_of_tensor_atMaximal

L32 ↗
AlgebraicGeometry.bijective_of_tensor_atMaximal
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 u
Lean source · statement
theorem bijective_of_tensor_atMaximal
    {R M N : Type u} [CommRing R] [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N] (F : M →ₗ[R] N)
    (h : ∀ (P : Ideal R) [P.IsMaximal],
      Function.Bijective (F.baseChange (Localization.AtPrime P))) :
    Function.Bijective F
theorem

isPushout_sections_of_proper_flat_of_etale_closedFiber

L56 ↗
AlgebraicGeometry.isPushout_sections_of_proper_flat_of_etale_closedFiber
Documentation

Arbitrary base change is a pushout of actual section maps for a proper flat Noetherian local family whose closed-fibre section algebra is étale.

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 u
Lean source · statement
theorem isPushout_sections_of_proper_flat_of_etale_closedFiber
    {S A : Type u} [CommRing S] [IsNoetherianRing S] [IsLocalRing S]
    [CommRing A] [Algebra S A] {Y : Scheme.{u}}
    (g : Y ⟶ Spec (CommRingCat.of S)) [IsProper g] [Flat g]
    (hEtaleFiber : (pullback.snd g
      (Spec.map (CommRingCat.ofHom (IsLocalRing.residue S)))).appTop.hom.Etale) :
    IsPushout (CommRingCat.ofHom (algebraMap S A))
      ((Scheme.ΓSpecIso (CommRingCat.of S)).inv ≫ g.appTop)
      ((Scheme.ΓSpecIso (CommRingCat.of A)).inv ≫
        (pullback.snd g (Spec.map (CommRingCat.ofHom (algebraMap S A)))).appTop)
      (pullback.fst g (Spec.map (CommRingCat.ofHom (algebraMap S A)))).appTop
theorem

isPushout_sections_of_proper_flat_noetherian_local_model

L95 ↗
AlgebraicGeometry.isPushout_sections_of_proper_flat_noetherian_local_model
Documentation

A geometrically reduced family over a local ring gives canonical section base change for any of its actual proper flat Noetherian local models.

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 u
Lean source · statement
theorem isPushout_sections_of_proper_flat_noetherian_local_model
    {S R : Type u} [CommRing S] [IsNoetherianRing S] [IsLocalRing S]
    [CommRing R] [IsLocalRing R] [Algebra S R] [IsLocalHom (algebraMap S R)]
    {Y X : Scheme.{u}} (g : Y ⟶ Spec (CommRingCat.of S)) [IsProper g] [Flat g]
    (f : X ⟶ Spec (CommRingCat.of R)) [GeometricallyReduced f] (p : X ⟶ Y)
    (hModel : IsPullback p f g (Spec.map (CommRingCat.ofHom (algebraMap S R)))) :
    IsPushout (CommRingCat.ofHom (algebraMap S R))
      ((Scheme.ΓSpecIso (CommRingCat.of S)).inv ≫ g.appTop)
      ((Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ f.appTop) p.appTop
theorem

isPushout_sections_of_proper_flat_noetherian_model_atPrime

L126 ↗
AlgebraicGeometry.isPushout_sections_of_proper_flat_noetherian_model_atPrime
Documentation

Localizing the original base of an actual Noetherian model gives canonical section base change. Only the original family after localization is required to have geometrically reduced fibres.

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 u
Lean source · statement
theorem isPushout_sections_of_proper_flat_noetherian_model_atPrime
    {S R : Type u} [CommRing S] [IsNoetherianRing S] [CommRing R] [Algebra S R]
    (P : Ideal R) [P.IsPrime] {Y X : Scheme.{u}}
    (g : Y ⟶ Spec (CommRingCat.of S)) [IsProper g] [Flat g]
    (f : X ⟶ Spec (CommRingCat.of (Localization.AtPrime P))) [GeometricallyReduced f]
    (p : X ⟶ Y)
    (hModel : IsPullback p f g
      (Spec.map (CommRingCat.ofHom (algebraMap S (Localization.AtPrime P))))) :
    IsPushout (CommRingCat.ofHom (algebraMap S (Localization.AtPrime P)))
      ((Scheme.ΓSpecIso (CommRingCat.of S)).inv ≫ g.appTop)
      ((Scheme.ΓSpecIso (CommRingCat.of (Localization.AtPrime P))).inv ≫ f.appTop)
      p.appTop
theorem

isPushout_sections_of_proper_flat_noetherian_model

L169 ↗
AlgebraicGeometry.isPushout_sections_of_proper_flat_noetherian_model
Documentation

The section algebra of a geometrically reduced family is the actual base change of the section algebra of any proper flat Noetherian model. The canonical comparison is checked at maximal ideals of the original base.

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 u
Lean source · statement
theorem isPushout_sections_of_proper_flat_noetherian_model
    {S R : Type u} [CommRing S] [IsNoetherianRing S] [CommRing R] [Algebra S R]
    {Y X : Scheme.{u}} (g : Y ⟶ Spec (CommRingCat.of S)) [IsProper g] [Flat g]
    (f : X ⟶ Spec (CommRingCat.of R)) [IsProper f] [GeometricallyReduced f]
    (p : X ⟶ Y)
    (hModel : IsPullback p f g (Spec.map (CommRingCat.ofHom (algebraMap S R)))) :
    IsPushout (CommRingCat.ofHom (algebraMap S R))
      ((Scheme.ΓSpecIso (CommRingCat.of S)).inv ≫ g.appTop)
      ((Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ f.appTop) p.appTop

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.