Documentation

TauCeti.AlgebraicGeometry.IdealSheaf.WeilRestriction

Weil restriction of a closed subscheme along a finite locally free morphism #

Let g : Y ⟶ S be finite locally free (finite, flat and locally of finite presentation) and let Z = V(I) ⊆ Y be a closed subscheme. For a scheme T over S, the base change Y_T = T ×_S Y ⟶ Y may or may not factor through Z. This file shows that the condition is represented by a closed subscheme of S: there is an ideal sheaf I.weilRestriction g on S such that Y_T ⟶ Y factors through Z exactly when T ⟶ S factors through its closed subscheme (AlgebraicGeometry.Scheme.IdealSheafData.weilRestriction_le_ker_iff). In other words, the Weil restriction of Z along g, which is a subfunctor of the Weil restriction S of Y itself, is a closed subscheme of S. Its formation commutes with arbitrary base change (AlgebraicGeometry.Scheme.IdealSheafData.weilRestriction_comap).

Over an affine open U ⊆ S, the ring B = Γ(Y, g⁻¹ U) is a finite projective module over A = Γ(S, U), and the ideal of I.weilRestriction g over U is the content of J = I(g⁻¹ U) ⊆ B: the ideal J.minorsIdeal 1 of A generated by the values φ x of all A-linear functionals φ : B → A at all x ∈ J (Submodule.minorsIdeal_one_le_iff). Over affine opens of T lying over U, the sections of Y_T are Γ(T, -) ⊗[A] B, and J vanishes there exactly when its content does (IsBaseChange.minorsIdeal_one_le_ker_iff).

Conditions of the form "a finite locally free family lies in a closed subscheme" are how the loci of Katz and Mazur are cut out: incidence of relative effective Cartier divisors, and the subgroup condition defining points of exact order N and Drinfeld level structures.

Main definitions #

Main results #

References #

source
noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.weilRestriction {Y S : Scheme} (g : Y ⟶ S) [IsFinite g] [Flat g] [LocallyOfFinitePresentation g] (I : Y.IdealSheafData) :
S.IdealSheafData

The ideal sheaf on S of the Weil restriction of the closed subscheme V(I) along a finite locally free morphism g : Y ⟶ S. A morphism T ⟶ S factors through its closed subscheme exactly when the base change T ×_S Y ⟶ Y factors through V(I) (AlgebraicGeometry.Scheme.IdealSheafData.weilRestriction_le_ker_iff). Over an affine open U of S, it is the content (the ideal of 1 × 1 minors) of the ideal I(g⁻¹ U) of the finite projective Γ(S, U)-module Γ(Y, g⁻¹ U).

Instances For
    source
    theorem AlgebraicGeometry.Scheme.IdealSheafData.weilRestriction_ideal {Y S : Scheme} (g : Y ⟶ S) [IsFinite g] [Flat g] [LocallyOfFinitePresentation g] (I : Y.IdealSheafData) (U : ↑S.affineOpens) :
    (weilRestriction g I).ideal U = (Submodule.restrictScalars (↑(S.presheaf.obj (Opposite.op ↑U))) (I.ideal ⟨(TopologicalSpace.Opens.map g.base).obj ↑U, ⋯⟩)).minorsIdeal 1

    Over an affine open U of S, the ideal of I.weilRestriction g is the content (the ideal of 1 × 1 minors) of the ideal I(g⁻¹ U) of the projective Γ(S, U)-module Γ(Y, g⁻¹ U).

    source
    theorem AlgebraicGeometry.Scheme.IdealSheafData.weilRestriction_mono {Y S : Scheme} (g : Y ⟶ S) [IsFinite g] [Flat g] [LocallyOfFinitePresentation g] :
    Monotone (weilRestriction g)

    The Weil restriction is monotone: a smaller closed subscheme has a smaller Weil restriction.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.IdealSheafData.weilRestriction_bot {Y S : Scheme} (g : Y ⟶ S) [IsFinite g] [Flat g] [LocallyOfFinitePresentation g] :
    weilRestriction g ⊥ = ⊥

    The Weil restriction of Y itself is S.

    source
    theorem AlgebraicGeometry.Scheme.IdealSheafData.weilRestriction_le_ker_iff {Y S : Scheme} (g : Y ⟶ S) [IsFinite g] [Flat g] [LocallyOfFinitePresentation g] (I : Y.IdealSheafData) {T : Scheme} (t : T ⟶ S) :
    weilRestriction g I ≤ Hom.ker t ↔ I ≤ Hom.ker (CategoryTheory.Limits.pullback.snd t g)

    The universal property of the Weil restriction of a closed subscheme. Let g : Y ⟶ S be finite locally free and I an ideal sheaf on Y. A morphism t : T ⟶ S factors through the closed subscheme of I.weilRestriction g exactly when the base change T ×_S Y ⟶ Y of t factors through the closed subscheme V(I).

    source
    theorem AlgebraicGeometry.Scheme.IdealSheafData.weilRestriction_le_ker_iff_of_isPullback {Y S : Scheme} {g : Y ⟶ S} [IsFinite g] [Flat g] [LocallyOfFinitePresentation g] (I : Y.IdealSheafData) {S' Y' : Scheme} {f : S' ⟶ S} {g' : Y' ⟶ S'} {gY : Y' ⟶ Y} (h : CategoryTheory.IsPullback g' gY f g) :
    weilRestriction g I ≤ Hom.ker f ↔ I ≤ Hom.ker gY

    The universal property of the Weil restriction, for a base change Y' of Y given by any pullback square: f : S' ⟶ S factors through the closed subscheme of I.weilRestriction g exactly when Y' ⟶ Y factors through V(I).

    source
    theorem AlgebraicGeometry.Scheme.IdealSheafData.weilRestriction_comap_le_ker_iff {Y S : Scheme} {g : Y ⟶ S} [IsFinite g] [Flat g] [LocallyOfFinitePresentation g] {X : Scheme} (J : X.IdealSheafData) (k : Y ⟶ X) {S' Y' X' : Scheme} {f : S' ⟶ S} {g' : Y' ⟶ S'} {gY : Y' ⟶ Y} (h : CategoryTheory.IsPullback g' gY f g) {k' : Y' ⟶ X'} {gX : X' ⟶ X} (w : CategoryTheory.CategoryStruct.comp k' gX = CategoryTheory.CategoryStruct.comp gY k) :
    weilRestriction g (J.comap k) ≤ Hom.ker f ↔ J.comap gX ≤ Hom.ker k'

    Closed conditions on finite locally free families. Let k : Y ⟶ X be a family over S parametrised by the finite locally free g : Y ⟶ S, and J an ideal sheaf on X. For a pullback square Y' ⟶ Y over f : S' ⟶ S and a morphism k' : Y' ⟶ X' lying over k along gX : X' ⟶ X, the base-changed family k' lies in the inverse image of V(J) exactly when f factors through the closed subscheme of the Weil restriction of V(J.comap k) along g.

    source
    theorem AlgebraicGeometry.Scheme.IdealSheafData.le_ker_pullback_snd_subschemeι_weilRestriction {Y S : Scheme} (g : Y ⟶ S) [IsFinite g] [Flat g] [LocallyOfFinitePresentation g] (I : Y.IdealSheafData) :
    I ≤ Hom.ker (CategoryTheory.Limits.pullback.snd (weilRestriction g I).subschemeι g)

    Over the closed subscheme of I.weilRestriction g, the base change of Y lies in the closed subscheme V(I): the universal family of the Weil restriction.

    source
    theorem AlgebraicGeometry.Scheme.IdealSheafData.weilRestriction_comap {Y S : Scheme} (g : Y ⟶ S) [IsFinite g] [Flat g] [LocallyOfFinitePresentation g] (I : Y.IdealSheafData) {T : Scheme} (t : T ⟶ S) :
    weilRestriction (CategoryTheory.Limits.pullback.fst t g) (I.comap (CategoryTheory.Limits.pullback.snd t g)) = (weilRestriction g I).comap t

    The Weil restriction of a closed subscheme commutes with base change. For t : T ⟶ S, the Weil restriction of the inverse image of V(I) in T ×_S Y along T ×_S Y ⟶ T is the inverse image of the Weil restriction of V(I) along g.