Module

LocalFactorOpenCover.lean

Nyll.SchemeTheory.Etale.LocalFactorOpenCover

4 declarations indexed from sourceView source ↗

Module documentation

Local factors on an actual open cover

Local lifts through a base-changed target map to lifts through the original target by the pullback projection. Local lifts on open-cover charts become local lifts on the glued source by taking their actual open images. No agreement between the different local lifts is required.

Imports6

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

Imported by3

theorem

of_pullback_snd

L33 ↗

AlgebraicGeometry.Scheme.Hom.ZariskiLocallyFactorsThrough.of_pullback_snd

Documentation

A local lift through a base-changed target gives a local lift through the original target after composing the source map with the base change.

Source context 4 commands

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

noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry

Lean source · statement

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

theorem

local_factor_on_open_image

L50 ↗

AlgebraicGeometry.local_factor_on_open_image

Source context 4 commands

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

noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry

Lean source · statement

theorem local_factor_on_open_image
    {A T U X : Scheme.{u}} (g : T ⟶ X) (f : U ⟶ X)
    (i : A ⟶ T) [IsOpenImmersion i] (a : A ⟶ U)
    (ha : a ≫ f = i ≫ g) (x : A) :
    ∃ V : T.Opens, i x ∈ V ∧ ∃ b : V.toScheme ⟶ U, b ≫ f = V.ι ≫ g

theorem

of_openCover

L70 ↗

AlgebraicGeometry.Scheme.Hom.ZariskiLocallyFactorsThrough.of_openCover

Documentation

Actual local factors on all charts of an open cover give actual local factors on the source. The neighborhoods are their open images.

Source context 4 commands

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

noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry

Lean source · statement

theorem Scheme.Hom.ZariskiLocallyFactorsThrough.of_openCover
    {T U X : Scheme.{u}} (g : T ⟶ X) (f : U ⟶ X)
    (𝒰 : Scheme.OpenCover.{v} T)
    (hlocal : ∀ i : 𝒰.I₀, (𝒰.f i ≫ g).ZariskiLocallyFactorsThrough f) :
    g.ZariskiLocallyFactorsThrough f

theorem

exists_sigma_factor

L88 ↗

AlgebraicGeometry.Scheme.Hom.ZariskiLocallyFactorsThrough.exists_sigma_factor

Documentation

Local factorization through a disjoint union refines near each source point to an actual factor through one member of the family.

Source context 4 commands

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

noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry

Lean source · statement

theorem Scheme.Hom.ZariskiLocallyFactorsThrough.exists_sigma_factor
    {X Y : Scheme.{u}} {I : Type u} (V : I → Scheme.{u})
    (f : ∀ i : I, V i ⟶ X) (q : Y ⟶ X)
    (hq : q.ZariskiLocallyFactorsThrough (Sigma.desc f)) (y : Y) :
    ∃ (W : Y.Opens), y ∈ W ∧ ∃ (i : I) (b : W.toScheme ⟶ V i),
      b ≫ f i = W.ι ≫ q

Module documentation

Local factors on an actual open cover

Declarations

of_pullback_snd

local_factor_on_open_image

of_openCover

exists_sigma_factor