Module

LocalFactorBaseChange.lean

Nyll.SchemeTheory.Etale.LocalFactorBaseChange

1 declaration indexed from sourceView source ↗

Module documentation

Base change of actual Zariski-local factorizations

Pull back the existing neighborhoods and their actual lifts, then use the native pullback universal property. In particular the original integral refinement's local factorizations remain available on every affine chart of a nonaffine base.

Imports4

Nyll.SchemeTheory.Etale.IntegralRefinement
Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.Restrict
Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Imported by2

theorem

baseChange

L31 ↗

AlgebraicGeometry.Scheme.Hom.ZariskiLocallyFactorsThrough.baseChange

Documentation

An actual local factorization survives arbitrary base change. The new local lift is constructed by the pullback universal property.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry

Lean source · statement

theorem Scheme.Hom.ZariskiLocallyFactorsThrough.baseChange
    {T U X Y : Scheme.{u}} {g : T ⟶ X} {f : U ⟶ X}
    (hlocal : g.ZariskiLocallyFactorsThrough f) (k : Y ⟶ X) :
    (pullback.snd g k).ZariskiLocallyFactorsThrough (pullback.snd f k)

Module documentation

Base change of actual Zariski-local factorizations

Declarations

baseChange