Module

NoetherianLocalProperModel.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.NoetherianLocalProperModel

1 declaration indexed from sourceView source ↗

Module documentation

An actual Noetherian local model of a proper flat finitely presented family

The existing finite-presentation approximation gives a proper flat model over a finitely generated integer algebra. The existing local-subalgebra construction makes its base Noetherian local inside the original local ring. Pullback cancellation gives the actual original family back.

Imports4

Nyll.AlgebraicCurves.Geometry.Schemes.exists_fg_subalgebra_isProper_flat_isPullback_of_isProper_of_flat_of_locallyOfFinitePresentation
Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_exists_subalgebra_coe_eq_isNoetherianRing_isLocalRing_isUnit_iff
Mathlib.Algebra.Ring.ULift
Mathlib.RingTheory.LocalRing.RingHom.Basic

Imported by2

theorem

exists_noetherian_local_proper_flat_model

L33 ↗

AlgebraicGeometry.exists_noetherian_local_proper_flat_model

Documentation

A proper flat finitely presented family over an arbitrary local ring comes from a proper flat family over an actual Noetherian local ring, along a local ring homomorphism.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open AlgebraicCurves.Geometry.Schemes.Proofs.ProperFlatFinitePresentationDescent.ApproxAux
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem exists_noetherian_local_proper_flat_model
    {R : Type u} [CommRing R] [IsLocalRing R] {X : Scheme.{u}}
    (f : X ⟶ Spec (CommRingCat.of R)) [IsProper f] [Flat f]
    [LocallyOfFinitePresentation f] :
    ∃ (S : Type u) (_ : CommRing S) (_ : IsNoetherianRing S) (_ : IsLocalRing S)
      (_ : Algebra S R) (_ : IsLocalHom (algebraMap S R)),
      ∃ (Y : Scheme.{u}) (g : Y ⟶ Spec (CommRingCat.of S)) (p : X ⟶ Y),
        IsProper g ∧ Flat g ∧
          IsPullback p f g (Spec.map (CommRingCat.ofHom (algebraMap S R)))

Module documentation

An actual Noetherian local model of a proper flat finitely presented family

Declarations

exists_noetherian_local_proper_flat_model