Module

BoundaryAwayPullback.lean

Nyll.EtaleFundamentalGroups.Inertia.BoundaryAwayPullback

3 declarations indexed from sourceView source ↗

Module documentation

Actual pullback squares for the boundary-away chart

The complement chart and the principal localization identify the same open subscheme as the inverse image of the original complement. Their canonical maps form pullback squares. This identifies the source of a base-changed relative normalization with the actual finite-etale pullback cover.

Imports4

Nyll.EtaleFundamentalGroups.Kummer.NormalCrossings.SchemeNormalCrossingsComplementCover
Nyll.SchemeTheory.Divisors.LocalComplement
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Imported by2

theorem

isPullback_comapSupportComplementTo

L30 ↗

AlgebraicGeometry.Scheme.IdealSheafData.isPullback_comapSupportComplementTo

Documentation

Pulling back an ideal's support complement is the actual complement square.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u

Lean source · statement

theorem isPullback_comapSupportComplementTo
    {X Y : Scheme.{u}} (I : X.IdealSheafData) (f : Y ⟶ X) :
    IsPullback (comapSupportComplementTo I f) (I.comap f).supportComplement.ι
      I.supportComplement.ι f

theorem

isPullback_localizationAwayToSupportComplement

L41 ↗

AlgebraicGeometry.Scheme.IdealSheafData.isPullback_localizationAwayToSupportComplement

Documentation

The principal local boundary complement is the pullback of the global support complement under the canonical localized-stalk map.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u

Lean source · statement

theorem isPullback_localizationAwayToSupportComplement
    {X : Scheme.{u}} (I : X.IdealSheafData) (x : X)
    (P : Ideal (X.presheaf.stalk x)) [P.IsPrime]
    (a : Localization.AtPrime P)
    (ha : (I.stalkIdeal x).map
      (algebraMap (X.presheaf.stalk x) (Localization.AtPrime P)) = Ideal.span {a}) :
    IsPullback (localizationAwayToSupportComplement I x P a ha)
      (Spec.map (CommRingCat.ofHom (algebraMap (Localization.AtPrime P) (Localization.Away a))))
      I.supportComplement.ι (Scheme.localizationAtPrimeTo X x P)

theorem

isPullback_boundaryAwayToSupportComplement

L58 ↗

AlgebraicGeometry.Scheme.IdealSheafData.isPullback_boundaryAwayToSupportComplement

Documentation

The composite boundary-away chart has the original support complement as its base-change square, including its canonical map into that complement.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u

Lean source · full declaration

theorem isPullback_boundaryAwayToSupportComplement
    {X Y : Scheme.{u}} (I : X.IdealSheafData) (f : Y ⟶ X) (y : Y)
    (P : Spec (Y.presheaf.stalk y)) :
    let : P.asIdeal.IsPrime := P.isPrime
    ∀ {r : ℕ} (t : Fin 2 → Localization.AtPrime P.asIdeal)
    (hboundary : ((I.comap f).stalkIdeal y).map
      (algebraMap (Y.presheaf.stalk y) (Localization.AtPrime P.asIdeal)) =
        Ideal.span {EtaleFundamentalGroups.boundaryProduct t r}),
    IsPullback (boundaryAwayToSupportComplement I f y P t hboundary)
      (Spec.map (CommRingCat.ofHom (algebraMap (Localization.AtPrime P.asIdeal)
        (Localization.Away (EtaleFundamentalGroups.boundaryProduct t r)))))
      I.supportComplement.ι (Scheme.localizationAtPrimeTo Y y P.asIdeal ≫ f) := by
  intro hP r t hboundary
  exact (isPullback_localizationAwayToSupportComplement (I.comap f) y P.asIdeal
    (EtaleFundamentalGroups.boundaryProduct t r) hboundary).paste_horiz
      (isPullback_comapSupportComplementTo I f)

Module documentation

Actual pullback squares for the boundary-away chart

Declarations

isPullback_comapSupportComplementTo

isPullback_localizationAwayToSupportComplement

isPullback_boundaryAwayToSupportComplement