NYLL
Module

RecoveredPullback.lean

Nyll.SchemeTheory.Gluing.RecoveredPullback
23 declarations indexed from sourceView source ↗

Module documentation

Actual recovered local charts and overlap maps after arbitrary base change.

Imports5
Imported by7

Declarations

def

swappedPullbackCover

L23 ↗
AlgebraicGeometry.Scheme.Cover.swappedPullbackCover
Documentation

The pulled-back cover with charts in the order used by Over.pullback.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
Lean source · statement
def swappedPullbackCover : Y.OpenCover
def

gluingLocalOver

L32 ↗
AlgebraicGeometry.Scheme.Cover.gluingLocalOver
Documentation

A local model viewed as a scheme over the original base.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
Lean source · statement
def gluingLocalOver (i : 𝒰.I₀) : Over X
def

gluingChartOver

L34 ↗
AlgebraicGeometry.Scheme.Cover.gluingChartOver
Documentation

An open chart viewed as a scheme over the original base.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
Lean source · statement
def gluingChartOver (i : 𝒰.I₀) : Over X
def

gluingLocalStructure

L36 ↗
AlgebraicGeometry.Scheme.Cover.gluingLocalStructure
Documentation

The structure map from a local model to its open chart.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
Lean source · statement
def gluingLocalStructure (i : 𝒰.I₀) : gluingLocalOver 𝒰 M i ⟶ gluingChartOver 𝒰 i
def

gluingOverlapOver

L40 ↗
AlgebraicGeometry.Scheme.Cover.gluingOverlapOver
Documentation

The overlap of a local model with a second open chart.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
Lean source · statement
def gluingOverlapOver (ij : 𝒰.I₀ × 𝒰.I₀) : Over X
def

gluingOverlapFirst

L45 ↗
AlgebraicGeometry.Scheme.Cover.gluingOverlapFirst
Documentation

The first projection from a local overlap to its model.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
Lean source · statement
def gluingOverlapFirst (i j : 𝒰.I₀) : gluingOverlapOver 𝒰 M (i, j) ⟶ gluingLocalOver 𝒰 M i
def

gluingOverlapSecond

L49 ↗
AlgebraicGeometry.Scheme.Cover.gluingOverlapSecond
Documentation

The second projection from a local overlap to its open chart.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
Lean source · statement
def gluingOverlapSecond (i j : 𝒰.I₀) : gluingOverlapOver 𝒰 M (i, j) ⟶ gluingChartOver 𝒰 j
theorem

overPullback_product_isPullback

L53 ↗
AlgebraicGeometry.Scheme.Cover.overPullback_product_isPullback
Documentation

The literal pullback of a relative product is the product over the new base.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
Lean source · statement
theorem overPullback_product_isPullback {P A C : Over X}
    (d : P ⟶ A) (r : P ⟶ C) (h : IsPullback d.left r.left A.hom C.hom) :
    IsPullback ((Over.pullback ψ).map d).left ((Over.pullback ψ).map r).left
      ((Over.pullback ψ).obj A).hom ((Over.pullback ψ).obj C).hom
theorem

recoveredPullbackOverlap_isPullback

L76 ↗
AlgebraicGeometry.Scheme.Cover.recoveredPullbackOverlap_isPullback
Source context 6 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
Lean source · statement
theorem recoveredPullbackOverlap_isPullback (i j : 𝒰.I₀) :
    IsPullback ((Over.pullback ψ).map (gluingOverlapFirst 𝒰 M i j)).left
      ((Over.pullback ψ).map (gluingOverlapSecond 𝒰 M i j)).left
      ((Over.pullback ψ).obj (gluingLocalOver 𝒰 M i)).hom
      ((Over.pullback ψ).obj (gluingChartOver 𝒰 j)).hom
def

recoveredPullbackLocalModel

L85 ↗
AlgebraicGeometry.Scheme.Cover.recoveredPullbackLocalModel
Documentation

The pulled-back local model over its pulled-back chart.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
Lean source · statement
def recoveredPullbackLocalModel (i : 𝒰.I₀) : Over ((swappedPullbackCover ψ 𝒰).X i)
def

recoveredPullbackLocalModelIso

L89 ↗
AlgebraicGeometry.Scheme.Cover.recoveredPullbackLocalModelIso
Documentation

The canonical iterated-pullback comparison for the local model.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
Lean source · statement
def recoveredPullbackLocalModelIso (i : 𝒰.I₀) :
    recoveredPullbackLocalModel ψ 𝒰 M i ≅
      (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i)
def

recoveredPullbackLocalIso

L114 ↗
AlgebraicGeometry.Scheme.Cover.recoveredPullbackLocalIso
Documentation

The given local recovery transported to the standard pullback chart.

Source context 8 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
Lean source · statement
def recoveredPullbackLocalIso (i : 𝒰.I₀) :
    recoveredPullbackLocalModel ψ 𝒰 M i ≅
      (Over.pullback ((swappedPullbackCover ψ 𝒰).f i)).obj Z
def

recoveredPullbackChartMap

L120 ↗
AlgebraicGeometry.Scheme.Cover.recoveredPullbackChartMap
Documentation

The recovered chart map into the original object after base change.

Source context 8 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
Lean source · statement
def recoveredPullbackChartMap (i : 𝒰.I₀) :
    ((Over.pullback ψ).obj (gluingLocalOver 𝒰 M i)).left ⟶ Z.left
def

recoveredPullbackChartCover

L126 ↗
AlgebraicGeometry.Scheme.Cover.recoveredPullbackChartCover
Documentation

The open cover supplied by the recovered local models.

Source context 8 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
Lean source · statement
def recoveredPullbackChartCover : Z.left.OpenCover
theorem

recoveredPullbackChartMap_isOpenImmersion

L130 ↗
AlgebraicGeometry.Scheme.Cover.recoveredPullbackChartMap_isOpenImmersion
Source context 8 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
Lean source · statement
theorem recoveredPullbackChartMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredPullbackChartMap ψ 𝒰 M Z e i)
theorem

recoveredPullbackChartMap_isPullback

L134 ↗
AlgebraicGeometry.Scheme.Cover.recoveredPullbackChartMap_isPullback
Source context 8 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
Lean source · statement
theorem recoveredPullbackChartMap_isPullback (i : 𝒰.I₀) :
    IsPullback ((Over.pullback ψ).map (gluingLocalStructure 𝒰 M i)).left
      (recoveredPullbackChartMap ψ 𝒰 M Z e i)
      (((Over.pullback ψ).obj (gluingChartOver 𝒰 i)).hom) Z.hom
theorem

recoveredPullbackChartMap_structure

L141 ↗
AlgebraicGeometry.Scheme.Cover.recoveredPullbackChartMap_structure
Source context 8 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
Lean source · statement
theorem recoveredPullbackChartMap_structure (i : 𝒰.I₀) :
    recoveredPullbackChartMap ψ 𝒰 M Z e i ≫ Z.hom =
      ((Over.pullback ψ).obj (gluingLocalOver 𝒰 M i)).hom
def

recoveredPullbackOverlapTransfer

L148 ↗
AlgebraicGeometry.Scheme.Cover.recoveredPullbackOverlapTransfer
Documentation

The map from a recovered overlap to its second local model.

Source context 8 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
Lean source · statement
def recoveredPullbackOverlapTransfer (i j : 𝒰.I₀) :
    ((Over.pullback ψ).obj (gluingOverlapOver 𝒰 M (i, j))).left ⟶
      ((Over.pullback ψ).obj (gluingLocalOver 𝒰 M j)).left
theorem

recoveredPullbackOverlapTransfer_structure

L160 ↗
AlgebraicGeometry.Scheme.Cover.recoveredPullbackOverlapTransfer_structure
Source context 8 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
Lean source · statement
theorem recoveredPullbackOverlapTransfer_structure (i j : 𝒰.I₀) :
    recoveredPullbackOverlapTransfer ψ 𝒰 M Z e i j ≫
      ((Over.pullback ψ).map (gluingLocalStructure 𝒰 M j)).left =
        ((Over.pullback ψ).map (gluingOverlapSecond 𝒰 M i j)).left
theorem

recoveredPullbackOverlapTransfer_chartMap

L167 ↗
AlgebraicGeometry.Scheme.Cover.recoveredPullbackOverlapTransfer_chartMap
Source context 8 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
Lean source · statement
theorem recoveredPullbackOverlapTransfer_chartMap (i j : 𝒰.I₀) :
    recoveredPullbackOverlapTransfer ψ 𝒰 M Z e i j ≫ recoveredPullbackChartMap ψ 𝒰 M Z e j =
      ((Over.pullback ψ).map (gluingOverlapFirst 𝒰 M i j)).left ≫
        recoveredPullbackChartMap ψ 𝒰 M Z e i
def

recoveredPullbackTransition

L174 ↗
AlgebraicGeometry.Scheme.Cover.recoveredPullbackTransition
Documentation

The transition map between the two orders of a recovered overlap.

Source context 8 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
Lean source · statement
def recoveredPullbackTransition (i j : 𝒰.I₀) :
    (Over.pullback ψ).obj (gluingOverlapOver 𝒰 M (i, j)) ⟶
      (Over.pullback ψ).obj (gluingOverlapOver 𝒰 M (j, i))
theorem

recoveredPullbackTransition_first

L193 ↗
AlgebraicGeometry.Scheme.Cover.recoveredPullbackTransition_first
Source context 8 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
Lean source · statement
theorem recoveredPullbackTransition_first (i j : 𝒰.I₀) :
    (recoveredPullbackTransition ψ 𝒰 M Z e i j).left ≫
      ((Over.pullback ψ).map (gluingOverlapFirst 𝒰 M j i)).left =
      recoveredPullbackOverlapTransfer ψ 𝒰 M Z e i j
theorem

recoveredPullbackTransition_chartMap

L199 ↗
AlgebraicGeometry.Scheme.Cover.recoveredPullbackTransition_chartMap
Source context 8 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
Lean source · statement
theorem recoveredPullbackTransition_chartMap (i j : 𝒰.I₀) :
    (recoveredPullbackTransition ψ 𝒰 M Z e i j).left ≫
      ((Over.pullback ψ).map (gluingOverlapFirst 𝒰 M j i)).left ≫
        recoveredPullbackChartMap ψ 𝒰 M Z e j =
      ((Over.pullback ψ).map (gluingOverlapFirst 𝒰 M i j)).left ≫
        recoveredPullbackChartMap ψ 𝒰 M Z e i

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