NYLL
Module

RecoveredLocalModel.lean

Nyll.SchemeTheory.Gluing.RecoveredLocalModel
27 declarations indexed from sourceView source ↗

Module documentation

Recovering overlaps from cartesian local models

Imports4
Imported by3

Declarations

def

recoveredChartIso

L25 ↗
AlgebraicGeometry.Scheme.Cover.recoveredChartIso
Source context 7 commands

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

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

recoveredChartIso_hom_structure

L30 ↗
AlgebraicGeometry.Scheme.Cover.recoveredChartIso_hom_structure
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
Lean source · statement
theorem recoveredChartIso_hom_structure (i : 𝒰.I₀) :
    (recoveredChartIso 𝒰 Z M e i).hom ≫ Limits.pullback.snd Z.hom (𝒰.f i) =
      (M i).hom
theorem

recoveredChartIso_inv_structure

L36 ↗
AlgebraicGeometry.Scheme.Cover.recoveredChartIso_inv_structure
Source context 7 commands

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

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

recoveredLocalModelMap

L42 ↗
AlgebraicGeometry.Scheme.Cover.recoveredLocalModelMap
Documentation

The map from a recovered local model to the original scheme.

Source context 7 commands

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

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

recoveredLocalModelMap_isOpenImmersion

L45 ↗
AlgebraicGeometry.Scheme.Cover.recoveredLocalModelMap_isOpenImmersion
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
Lean source · statement
instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i)
theorem

recoveredLocalModelMap_structure

L51 ↗
AlgebraicGeometry.Scheme.Cover.recoveredLocalModelMap_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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · statement
theorem recoveredLocalModelMap_structure (i : 𝒰.I₀) :
    recoveredLocalModelMap 𝒰 Z M e i ≫ Z.hom = (M i).hom ≫ 𝒰.f i
theorem

recoveredLocalModelMap_isPullback

L57 ↗
AlgebraicGeometry.Scheme.Cover.recoveredLocalModelMap_isPullback
Documentation

Each actual recovered chart is cartesian over its base 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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · statement
theorem recoveredLocalModelMap_isPullback (i : 𝒰.I₀) :
    IsPullback (M i).hom (recoveredLocalModelMap 𝒰 Z M e i) (𝒰.f i) Z.hom
abbrev

recoveredOverlap

L67 ↗
AlgebraicGeometry.Scheme.Cover.recoveredOverlap
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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · statement
abbrev recoveredOverlap (i j : 𝒰.I₀) : Scheme.{u}
def

recoveredOverlapTransfer

L70 ↗
AlgebraicGeometry.Scheme.Cover.recoveredOverlapTransfer
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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · statement
def recoveredOverlapTransfer (i j : 𝒰.I₀) :
    recoveredOverlap 𝒰 M i j ⟶ (M j).left
theorem

recoveredOverlapTransfer_structure

L80 ↗
AlgebraicGeometry.Scheme.Cover.recoveredOverlapTransfer_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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · statement
theorem recoveredOverlapTransfer_structure (i j : 𝒰.I₀) :
    recoveredOverlapTransfer 𝒰 Z M e i j ≫ (M j).hom =
      Limits.pullback.snd ((M i).hom ≫ 𝒰.f i) (𝒰.f j)
theorem

recoveredOverlapTransfer_chartMap

L87 ↗
AlgebraicGeometry.Scheme.Cover.recoveredOverlapTransfer_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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · statement
theorem recoveredOverlapTransfer_chartMap (i j : 𝒰.I₀) :
    recoveredOverlapTransfer 𝒰 Z M e i j ≫ recoveredLocalModelMap 𝒰 Z M e j =
      Limits.pullback.fst ((M i).hom ≫ 𝒰.f i) (𝒰.f j) ≫
        recoveredLocalModelMap 𝒰 Z M e i
def

recoveredOverlapTransition

L94 ↗
AlgebraicGeometry.Scheme.Cover.recoveredOverlapTransition
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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · statement
def recoveredOverlapTransition (i j : 𝒰.I₀) :
    recoveredOverlap 𝒰 M i j ⟶ recoveredOverlap 𝒰 M j i
theorem

recoveredOverlapTransition_fst

L104 ↗
AlgebraicGeometry.Scheme.Cover.recoveredOverlapTransition_fst
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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · statement
theorem recoveredOverlapTransition_fst (i j : 𝒰.I₀) :
    recoveredOverlapTransition 𝒰 Z M e i j ≫
      Limits.pullback.fst ((M j).hom ≫ 𝒰.f j) (𝒰.f i) =
        recoveredOverlapTransfer 𝒰 Z M e i j
theorem

recoveredOverlapTransition_snd

L111 ↗
AlgebraicGeometry.Scheme.Cover.recoveredOverlapTransition_snd
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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · statement
theorem recoveredOverlapTransition_snd (i j : 𝒰.I₀) :
    recoveredOverlapTransition 𝒰 Z M e i j ≫
      Limits.pullback.snd ((M j).hom ≫ 𝒰.f j) (𝒰.f i) =
        Limits.pullback.fst ((M i).hom ≫ 𝒰.f i) (𝒰.f j) ≫ (M i).hom
theorem

recoveredOverlapTransition_chartMap

L118 ↗
AlgebraicGeometry.Scheme.Cover.recoveredOverlapTransition_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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · statement
theorem recoveredOverlapTransition_chartMap (i j : 𝒰.I₀) :
    recoveredOverlapTransition 𝒰 Z M e i j ≫
      Limits.pullback.fst ((M j).hom ≫ 𝒰.f j) (𝒰.f i) ≫
        recoveredLocalModelMap 𝒰 Z M e j =
    Limits.pullback.fst ((M i).hom ≫ 𝒰.f i) (𝒰.f j) ≫
      recoveredLocalModelMap 𝒰 Z M e i
theorem

recoveredOverlapTransition_id

L126 ↗
AlgebraicGeometry.Scheme.Cover.recoveredOverlapTransition_id
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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · statement
theorem recoveredOverlapTransition_id (i : 𝒰.I₀) :
    recoveredOverlapTransition 𝒰 Z M e i i = 𝟙 _
abbrev

recoveredTriple

L132 ↗
AlgebraicGeometry.Scheme.Cover.recoveredTriple
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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · statement
abbrev recoveredTriple (i j k : 𝒰.I₀) : Scheme.{u}
def

recoveredTripleToOverlap

L137 ↗
AlgebraicGeometry.Scheme.Cover.recoveredTripleToOverlap
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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · statement
def recoveredTripleToOverlap (i j k : 𝒰.I₀) :
    recoveredTriple 𝒰 M i j k ⟶ recoveredOverlap 𝒰 M j k
def

recoveredTripleTransition

L149 ↗
AlgebraicGeometry.Scheme.Cover.recoveredTripleTransition
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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · statement
def recoveredTripleTransition (i j k : 𝒰.I₀) :
    recoveredTriple 𝒰 M i j k ⟶ recoveredTriple 𝒰 M j k i
theorem

recoveredTripleTransition_chartMap

L159 ↗
AlgebraicGeometry.Scheme.Cover.recoveredTripleTransition_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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · statement
theorem recoveredTripleTransition_chartMap (i j k : 𝒰.I₀) :
    recoveredTripleTransition 𝒰 Z M e i j k ≫
      Limits.pullback.fst _ _ ≫
        Limits.pullback.fst ((M j).hom ≫ 𝒰.f j) (𝒰.f k) ≫
          recoveredLocalModelMap 𝒰 Z M e j =
    Limits.pullback.fst _ _ ≫
      Limits.pullback.fst ((M i).hom ≫ 𝒰.f i) (𝒰.f j) ≫
        recoveredLocalModelMap 𝒰 Z M e i
theorem

recoveredTripleTransition_cocycle

L170 ↗
AlgebraicGeometry.Scheme.Cover.recoveredTripleTransition_cocycle
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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · statement
theorem recoveredTripleTransition_cocycle (i j k : 𝒰.I₀) :
    recoveredTripleTransition 𝒰 Z M e i j k ≫
      recoveredTripleTransition 𝒰 Z M e j k i ≫
        recoveredTripleTransition 𝒰 Z M e k i j = 𝟙 _
def

recoveredOverlapGlueData

L184 ↗
AlgebraicGeometry.Scheme.Cover.recoveredOverlapGlueData
Documentation

Actual local models recovered from one scheme determine gluing data on their literal pairwise overlaps, including the diagonal and triple cocycle laws.

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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · full declaration
def recoveredOverlapGlueData : Scheme.GlueData.{u} where
  J := 𝒰.I₀
  U i := (M i).left
  V ij := recoveredOverlap 𝒰 M ij.1 ij.2
  f i j := Limits.pullback.fst ((M i).hom ≫ 𝒰.f i) (𝒰.f j)
  f_id i := inferInstance
  t i j := recoveredOverlapTransition 𝒰 Z M e i j
  t_id i := recoveredOverlapTransition_id 𝒰 Z M e i
  t' i j k := recoveredTripleTransition 𝒰 Z M e i j k
  t_fac i j k := Limits.pullback.lift_snd _ _ _
  cocycle i j k := recoveredTripleTransition_cocycle 𝒰 Z M e i j k
  f_open i j := inferInstance
theorem

recoveredOverlapGlueData_transition_structure

L199 ↗
AlgebraicGeometry.Scheme.Cover.recoveredOverlapGlueData_transition_structure
Documentation

The recovered transition preserves the actual structure map to the other base 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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · statement
theorem recoveredOverlapGlueData_transition_structure (i j : 𝒰.I₀) :
    (recoveredOverlapGlueData 𝒰 Z M e).t i j ≫
      (recoveredOverlapGlueData 𝒰 Z M e).f j i ≫ (M j).hom =
        Limits.pullback.snd ((M i).hom ≫ 𝒰.f i) (𝒰.f j)
theorem

recoveredOverlapGlueData_transition_map

L208 ↗
AlgebraicGeometry.Scheme.Cover.recoveredOverlapGlueData_transition_map
Documentation

The local maps to the original scheme agree on the recovered overlaps.

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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · statement
theorem recoveredOverlapGlueData_transition_map (i j : 𝒰.I₀) :
    (recoveredOverlapGlueData 𝒰 Z M e).t i j ≫
      (recoveredOverlapGlueData 𝒰 Z M e).f j i ≫ recoveredLocalModelMap 𝒰 Z M e j =
    (recoveredOverlapGlueData 𝒰 Z M e).f i j ≫ recoveredLocalModelMap 𝒰 Z M e i
theorem

recoveredOverlapGlueData_transition_base

L215 ↗
AlgebraicGeometry.Scheme.Cover.recoveredOverlapGlueData_transition_base
Documentation

The recovered transition preserves the structure map to the covered base.

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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · statement
theorem recoveredOverlapGlueData_transition_base (i j : 𝒰.I₀) :
    (recoveredOverlapGlueData 𝒰 Z M e).t i j ≫
      (recoveredOverlapGlueData 𝒰 Z M e).f j i ≫ (M j).hom ≫ 𝒰.f j =
    (recoveredOverlapGlueData 𝒰 Z M e).f i j ≫ (M i).hom ≫ 𝒰.f i
theorem

recoveredOverlapGlueData_isPullback

L226 ↗
AlgebraicGeometry.Scheme.Cover.recoveredOverlapGlueData_isPullback
Documentation

The recovered overlap is the actual intersection of the two recovered charts.

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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · statement
theorem recoveredOverlapGlueData_isPullback (i j : 𝒰.I₀) :
    IsPullback ((recoveredOverlapGlueData 𝒰 Z M e).f i j)
      ((recoveredOverlapGlueData 𝒰 Z M e).t i j ≫
        (recoveredOverlapGlueData 𝒰 Z M e).f j i)
      (recoveredLocalModelMap 𝒰 Z M e i) (recoveredLocalModelMap 𝒰 Z M e j)
def

recoveredLocalModelCover

L244 ↗
AlgebraicGeometry.Scheme.Cover.recoveredLocalModelCover
Documentation

The recovered local models form an actual open cover of the original scheme.

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 {S : Scheme.{u}} (𝒰 : S.OpenCover) (Z : Over S)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (e : ∀ i : 𝒰.I₀, M i ≅ (Over.pullback (𝒰.f i)).obj Z)
local instance recoveredLocalModelMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredLocalModelMap 𝒰 Z M e i) := by
  dsimp only [recoveredLocalModelMap]
  infer_instance
Lean source · full declaration
def recoveredLocalModelCover : Z.left.OpenCover where
  I₀ := 𝒰.I₀
  X i := (M i).left
  f i := recoveredLocalModelMap 𝒰 Z M e i
  mem₀ := by
    rw [presieve₀_mem_precoverage_iff]
    refine ⟨?_, fun i => inferInstance⟩
    intro z
    obtain ⟨i, x, hx⟩ := 𝒰.exists_eq (Z.hom z)
    obtain ⟨v, hv, -⟩ := Scheme.Pullback.exists_preimage_pullback z x hx.symm
    refine ⟨i, (recoveredChartIso 𝒰 Z M e i).inv v, ?_⟩
    rw [← Scheme.Hom.comp_apply]
    change ((recoveredChartIso 𝒰 Z M e i).inv ≫
      (recoveredChartIso 𝒰 Z M e i).hom ≫ Limits.pullback.fst Z.hom (𝒰.f i)) v = z
    rw [Iso.inv_hom_id_assoc]
    exact hv

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