NYLL
Module

RelativePullback.lean

Nyll.SchemeTheory.Gluing.RelativePullback
5 declarations indexed from sourceView source ↗

Module documentation

Scheme gluing after actual pullback equations

Once the diagonal and triple relations have been proved after a base change, the transported cartesian overlap maps form actual scheme gluing data. The triple comparison construction adapts GlueData.mapGlueData: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/CategoryTheory/GlueData.lean

The inverse-limit consumer supplies both relations using actual eventual equality, with no equality-reflection assumption on the limit projection.

Imports3
Imported by3

Declarations

theorem

relativePullback_map_isPullback

L34 ↗
AlgebraicGeometry.Scheme.Cover.relativePullback_map_isPullback
Documentation

The native pullback of a morphism over the base is cartesian over its original underlying morphism.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
Lean source · statement
theorem relativePullback_map_isPullback
    {B B' : Scheme.{u}} (ψ : B' ⟶ B) {A C : Over B} (m : A ⟶ C) :
    IsPullback ((Over.pullback ψ).map m).left (pullback.fst A.hom ψ)
      (pullback.fst C.hom ψ) m.left
def

relativeGlueDataOfPullbackEquations

L66 ↗
AlgebraicGeometry.Scheme.Cover.relativeGlueDataOfPullbackEquations
Documentation

Actual relative gluing data after the diagonal and triple equations have been established by pullback.

Source context 15 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
variable {B S B' : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
variable (ψ : B' ⟶ B)
variable (hdiag : ∀ i : 𝒰.I₀,
  (Over.pullback ψ).map (t i i) = 𝟙 ((Over.pullback ψ).obj (V (i, i))))
variable (hcycle : ∀ i j k : 𝒰.I₀,
  (Over.pullback ψ).map
      (relativeTripleTransition 𝒰 A V d y ℓ hV t ht i j k ≫
        relativeTripleTransition 𝒰 A V d y ℓ hV t ht j k i ≫
          relativeTripleTransition 𝒰 A V d y ℓ hV t ht k i j) =
    𝟙 ((Over.pullback ψ).obj (relativeTriple 𝒰 A V d i j k)))
Lean source · statement
def relativeGlueDataOfPullbackEquations : Scheme.GlueData.{u}
theorem

relativeGlueDataOfPullbackEquations_U

L110 ↗
AlgebraicGeometry.Scheme.Cover.relativeGlueDataOfPullbackEquations_U
Documentation

The glued charts are the actual pullbacks of the original local models.

Source context 15 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
variable {B S B' : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
variable (ψ : B' ⟶ B)
variable (hdiag : ∀ i : 𝒰.I₀,
  (Over.pullback ψ).map (t i i) = 𝟙 ((Over.pullback ψ).obj (V (i, i))))
variable (hcycle : ∀ i j k : 𝒰.I₀,
  (Over.pullback ψ).map
      (relativeTripleTransition 𝒰 A V d y ℓ hV t ht i j k ≫
        relativeTripleTransition 𝒰 A V d y ℓ hV t ht j k i ≫
          relativeTripleTransition 𝒰 A V d y ℓ hV t ht k i j) =
    𝟙 ((Over.pullback ψ).obj (relativeTriple 𝒰 A V d i j k)))
Lean source · statement
theorem relativeGlueDataOfPullbackEquations_U (i : 𝒰.I₀) :
    (relativeGlueDataOfPullbackEquations 𝒰 A V d y ℓ hV t ht ψ hdiag hcycle).U i =
      (relativeRecoveryFunctor ψ).obj (A i)
theorem

relativeGlueDataOfPullbackEquations_f

L115 ↗
AlgebraicGeometry.Scheme.Cover.relativeGlueDataOfPullbackEquations_f
Documentation

The glued overlap inclusions are the actual pulled-back inclusions.

Source context 15 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
variable {B S B' : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
variable (ψ : B' ⟶ B)
variable (hdiag : ∀ i : 𝒰.I₀,
  (Over.pullback ψ).map (t i i) = 𝟙 ((Over.pullback ψ).obj (V (i, i))))
variable (hcycle : ∀ i j k : 𝒰.I₀,
  (Over.pullback ψ).map
      (relativeTripleTransition 𝒰 A V d y ℓ hV t ht i j k ≫
        relativeTripleTransition 𝒰 A V d y ℓ hV t ht j k i ≫
          relativeTripleTransition 𝒰 A V d y ℓ hV t ht k i j) =
    𝟙 ((Over.pullback ψ).obj (relativeTriple 𝒰 A V d i j k)))
Lean source · statement
theorem relativeGlueDataOfPullbackEquations_f (i j : 𝒰.I₀) :
    (relativeGlueDataOfPullbackEquations 𝒰 A V d y ℓ hV t ht ψ hdiag hcycle).f i j =
      (relativeRecoveryFunctor ψ).map (d i j)
theorem

relativeGlueDataOfPullbackEquations_t

L120 ↗
AlgebraicGeometry.Scheme.Cover.relativeGlueDataOfPullbackEquations_t
Documentation

The glued transition maps are the actual pulled-back transitions.

Source context 15 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
variable {B S B' : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
variable (ψ : B' ⟶ B)
variable (hdiag : ∀ i : 𝒰.I₀,
  (Over.pullback ψ).map (t i i) = 𝟙 ((Over.pullback ψ).obj (V (i, i))))
variable (hcycle : ∀ i j k : 𝒰.I₀,
  (Over.pullback ψ).map
      (relativeTripleTransition 𝒰 A V d y ℓ hV t ht i j k ≫
        relativeTripleTransition 𝒰 A V d y ℓ hV t ht j k i ≫
          relativeTripleTransition 𝒰 A V d y ℓ hV t ht k i j) =
    𝟙 ((Over.pullback ψ).obj (relativeTriple 𝒰 A V d i j k)))
Lean source · statement
theorem relativeGlueDataOfPullbackEquations_t (i j : 𝒰.I₀) :
    (relativeGlueDataOfPullbackEquations 𝒰 A V d y ℓ hV t ht ψ hdiag hcycle).t i j =
      (relativeRecoveryFunctor ψ).map (t i j)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.