NYLL
Module

AffineFiniteSubalgebraRefinement.lean

Nyll.SchemeTheory.Etale.AffineFiniteSubalgebraRefinement
2 declarations indexed from sourceView source ↗

Module documentation

Actual finite subalgebras retaining the original local factorizations

The existing affine finite-presentation descent produces a finite stage with an actual map to the original integral algebra. Taking that map's image produces a finite subalgebra of the original algebra. Its spectrum inherits the local factorizations by pulling back their actual open sets.

This supplies local finite subalgebras for global submodule extension; it does not reconstruct affine descent or assert that the subalgebras already extend compatibly across a nonaffine base.

Imports6
Imported by3

Declarations

theorem

precomp

L37 ↗
AlgebraicGeometry.Scheme.Hom.ZariskiLocallyFactorsThrough.precomp
Documentation

Pulling back the actual neighborhoods and their lifts preserves Zariski-local factorization through a fixed morphism.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Opposite Algebra
namespace AlgebraicGeometry
Lean source · statement
theorem Scheme.Hom.ZariskiLocallyFactorsThrough.precomp {S T U X : Scheme.{u}}
    {g : T ⟶ X} {f : U ⟶ X} (h : g.ZariskiLocallyFactorsThrough f) (k : S ⟶ T) :
    (k ≫ g).ZariskiLocallyFactorsThrough f
theorem

exists_finite_subalgebra_locally_factors

L58 ↗
AlgebraicGeometry.AffineIntegralLimit.exists_finite_subalgebra_locally_factors
Documentation

Actual local factorizations of the original integral spectrum descend to a finite subalgebra inside the original algebra, rather than merely to an abstract finite-presentation stage mapping to it.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite Algebra
namespace AlgebraicGeometry
namespace AffineIntegralLimit
Lean source · statement
theorem exists_finite_subalgebra_locally_factors
    {R B : Type u} [CommRing R] [CommRing B] [Algebra R B] [Algebra.IsIntegral R B]
    {U : Scheme.{u}} (f : U ⟶ Spec (CommRingCat.of R)) [LocallyOfFinitePresentation f]
    (hlocal : (Spec.map (CommRingCat.ofHom (algebraMap R B))).ZariskiLocallyFactorsThrough f) :
    ∃ C : Subalgebra R B, Module.Finite R C ∧
      (Spec.map (CommRingCat.ofHom (algebraMap R C))).ZariskiLocallyFactorsThrough f

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