Module

RecoveredChartTransport.lean

Nyll.SchemeTheory.Gluing.RecoveredChartTransport

5 declarations indexed from sourceView source ↗

Module documentation

Transport of recovered charts through an actual natural isomorphism

Changing the base-change functor along a specified natural isomorphism preserves the recovered open cover, its cartesian structure squares, and the actual pairwise recovery equations.

Imports3

Mathlib.AlgebraicGeometry.Cover.Open
Mathlib.CategoryTheory.Comma.Over.Basic
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Imported by2

theorem

recoveredChartTransport_isOpenImmersion

L32 ↗

AlgebraicGeometry.Scheme.Cover.recoveredChartTransport_isOpenImmersion

Documentation

Precomposing a recovered chart with the inverse comparison preserves its open immersion into the recovered scheme.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.Cover
universe u v
variable {S L : Scheme.{u}}
variable {F G : Over S ⥤ Over L} (e : F ≅ G)

Lean source · statement

theorem recoveredChartTransport_isOpenImmersion
    {A : Over S} {Z : Over L} (h : F.obj A ⟶ Z) [IsOpenImmersion h.left] :
    IsOpenImmersion ((e.inv.app A ≫ h).left)

def

recoveredChartTransportOpenCover

L42 ↗

AlgebraicGeometry.Scheme.Cover.recoveredChartTransportOpenCover

Documentation

The transported family is an actual open cover, obtained by copying the original cover along the comparison isomorphisms.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.Cover
universe u v
variable {S L : Scheme.{u}}
variable {F G : Over S ⥤ Over L} (e : F ≅ G)

Lean source · statement

def recoveredChartTransportOpenCover
    {K : Type v} (A : K → Over S) (Z : Over L) (h : ∀ i, F.obj (A i) ⟶ Z)
    [∀ i, IsOpenImmersion (h i).left]
    (hcover : ∀ z : Z.left, ∃ (i : K) (x : (F.obj (A i)).left), (h i).left x = z) :
    Z.left.OpenCover

theorem

recoveredChartTransport_covers

L54 ↗

AlgebraicGeometry.Scheme.Cover.recoveredChartTransport_covers

Documentation

Every point is still in a transported chart.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.Cover
universe u v
variable {S L : Scheme.{u}}
variable {F G : Over S ⥤ Over L} (e : F ≅ G)

Lean source · statement

theorem recoveredChartTransport_covers
    {K : Type v} (A : K → Over S) (Z : Over L) (h : ∀ i, F.obj (A i) ⟶ Z)
    [∀ i, IsOpenImmersion (h i).left]
    (hcover : ∀ z : Z.left, ∃ (i : K) (x : (F.obj (A i)).left), (h i).left x = z)
    (z : Z.left) :
    ∃ (i : K) (x : (G.obj (A i)).left), (e.inv.app (A i) ≫ h i).left x = z

theorem

recoveredChartTransport_isPullback

L64 ↗

AlgebraicGeometry.Scheme.Cover.recoveredChartTransport_isPullback

Documentation

A recovered structural pullback square remains cartesian after transporting the base-change functor through the actual comparison.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.Cover
universe u v
variable {S L : Scheme.{u}}
variable {F G : Over S ⥤ Over L} (e : F ≅ G)

Lean source · statement

theorem recoveredChartTransport_isPullback
    {A U : Over S} {Z : Over L} (y : A ⟶ U) (h : F.obj A ⟶ Z)
    (hPB : IsPullback (F.map y).left h.left (F.obj U).hom Z.hom) :
    IsPullback (G.map y).left (e.inv.app A ≫ h).left (G.obj U).hom Z.hom

theorem

recoveredChartTransport_pair

L79 ↗

AlgebraicGeometry.Scheme.Cover.recoveredChartTransport_pair

Documentation

The pairwise recovered-chart equation is preserved by compatible transport of the overlap morphism. All maps are the original maps over the two bases; no faithfulness assumption is used.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.Cover
universe u v
variable {S L : Scheme.{u}}
variable {F G : Over S ⥤ Over L} (e : F ≅ G)

Lean source · statement

theorem recoveredChartTransport_pair
    {A B V W : Over S} {Z : Over L}
    (d : V ⟶ A) (r : W ⟶ B) (hA : F.obj A ⟶ Z) (hB : F.obj B ⟶ Z)
    (a : F.obj V ⟶ F.obj W) (b : G.obj V ⟶ G.obj W)
    (hab : e.hom.app V ≫ b = a ≫ e.hom.app W)
    (hrec : a ≫ F.map r ≫ hB = F.map d ≫ hA) :
    b ≫ G.map r ≫ (e.inv.app B ≫ hB) = G.map d ≫ (e.inv.app A ≫ hA)

Module documentation

Transport of recovered charts through an actual natural isomorphism

Declarations

recoveredChartTransport_isOpenImmersion

recoveredChartTransportOpenCover

recoveredChartTransport_covers

recoveredChartTransport_isPullback

recoveredChartTransport_pair