NYLL
Module

RelativeOverlap.lean

Nyll.SchemeTheory.Gluing.RelativeOverlap
12 declarations indexed from sourceView source ↗

Module documentation

Recovered relative-overlap equations

Actual cartesian pairwise overlaps produce triple transition maps. After an arbitrary base change, monic recovered chart maps prove the diagonal and triple equations. No faithfulness or surjectivity of the base change is used: these equations can subsequently be descended to a later stage.

Imports4
  • Mathlib.AlgebraicGeometry.PullbackCarrier
  • Mathlib.CategoryTheory.Comma.Over.Pullback
  • Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
  • Mathlib.AlgebraicGeometry.Cover.Open
Imported by5

Declarations

theorem

relativeOverlapInclusion_isOpenImmersion

L36 ↗
AlgebraicGeometry.Scheme.Cover.relativeOverlapInclusion_isOpenImmersion
Source context 11 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {B S : 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))
include hV in
Lean source · statement
theorem relativeOverlapInclusion_isOpenImmersion (i j : 𝒰.I₀) : IsOpenImmersion (d i j).left
theorem

relativeOverlapInclusion_mono

L40 ↗
AlgebraicGeometry.Scheme.Cover.relativeOverlapInclusion_mono
Source context 11 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {B S : 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))
include hV in
Lean source · statement
theorem relativeOverlapInclusion_mono (i j : 𝒰.I₀) : Mono (d i j)
theorem

relativeOverlapInclusion_isIso

L46 ↗
AlgebraicGeometry.Scheme.Cover.relativeOverlapInclusion_isIso
Source context 11 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {B S : 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))
include hV in
Lean source · statement
theorem relativeOverlapInclusion_isIso (i : 𝒰.I₀) : IsIso (d i i)
theorem

relativeOverlapTransition_structure

L58 ↗
AlgebraicGeometry.Scheme.Cover.relativeOverlapTransition_structure
Documentation

Preservation of the base gives the other chart structure equation.

Source context 13 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {B S : 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)
include hV in
Lean source · statement
theorem relativeOverlapTransition_structure
    (hS : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j ≫ 𝒰.f j =
      (d i j).left ≫ y i ≫ 𝒰.f i) (i j : 𝒰.I₀) :
    (t i j).left ≫ (d j i).left ≫ y j = ℓ i j
abbrev

relativeTriple

L67 ↗
AlgebraicGeometry.Scheme.Cover.relativeTriple
Documentation

The actual intersection of two overlap objects inside their first chart.

Source context 12 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {B S : 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)
Lean source · statement
abbrev relativeTriple (i j k : 𝒰.I₀) : Over B
def

relativeTripleToOverlap

L71 ↗
AlgebraicGeometry.Scheme.Cover.relativeTripleToOverlap
Documentation

The map from a triple intersection to the next pairwise overlap.

Source context 12 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {B S : 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)
Lean source · statement
def relativeTripleToOverlap (i j k : 𝒰.I₀) :
    relativeTriple 𝒰 A V d i j k ⟶ V (j, k)
def

relativeTripleTransition

L99 ↗
AlgebraicGeometry.Scheme.Cover.relativeTripleTransition
Documentation

The cyclic transition between actual triple intersection objects.

Source context 12 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {B S : 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)
Lean source · statement
def relativeTripleTransition (i j k : 𝒰.I₀) :
    relativeTriple 𝒰 A V d i j k ⟶ relativeTriple 𝒰 A V d j k i
theorem

relativeTripleTransition_fac

L108 ↗
AlgebraicGeometry.Scheme.Cover.relativeTripleTransition_fac
Source context 12 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {B S : 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)
Lean source · statement
theorem relativeTripleTransition_fac (i j k : 𝒰.I₀) :
    relativeTripleTransition 𝒰 A V d y ℓ hV t ht i j k ≫ pullback.snd _ _ =
      pullback.fst _ _ ≫ t i j
abbrev

relativeRecoveryFunctor

L116 ↗
AlgebraicGeometry.Scheme.Cover.relativeRecoveryFunctor
Documentation

Base change followed by forgetting the structure morphism.

Source context 13 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {B S : 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' Z : Scheme.{u}} (ψ : B' ⟶ B)
Lean source · statement
abbrev relativeRecoveryFunctor : Over B ⥤ Scheme.{u}
theorem

relativeRecoveredTransition_id

L129 ↗
AlgebraicGeometry.Scheme.Cover.relativeRecoveredTransition_id
Documentation

The diagonal transition is the identity after the actual recovering base change. No equality-reflection hypothesis is needed.

Source context 17 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {B S : 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' Z : Scheme.{u}} (ψ : B' ⟶ B)
variable (h : ∀ i : 𝒰.I₀, (relativeRecoveryFunctor ψ).obj (A i) ⟶ Z)
variable [∀ i : 𝒰.I₀, Mono (h i)]
variable (hrec : ∀ i j : 𝒰.I₀,
  (relativeRecoveryFunctor ψ).map (t i j) ≫
      (relativeRecoveryFunctor ψ).map (d j i) ≫ h j =
    (relativeRecoveryFunctor ψ).map (d i j) ≫ h i)
include hV hrec in
Lean source · statement
theorem relativeRecoveredTransition_id (i : 𝒰.I₀) :
    (relativeRecoveryFunctor ψ).map (t i i) =
      (relativeRecoveryFunctor ψ).map (𝟙 (V (i, i)))
theorem

relativeRecoveredTripleTransition_chartMap

L140 ↗
AlgebraicGeometry.Scheme.Cover.relativeRecoveredTripleTransition_chartMap
Documentation

The recovered triple transition preserves its actual chart map.

Source context 18 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {B S : 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' Z : Scheme.{u}} (ψ : B' ⟶ B)
variable (h : ∀ i : 𝒰.I₀, (relativeRecoveryFunctor ψ).obj (A i) ⟶ Z)
variable [∀ i : 𝒰.I₀, Mono (h i)]
variable (hrec : ∀ i j : 𝒰.I₀,
  (relativeRecoveryFunctor ψ).map (t i j) ≫
      (relativeRecoveryFunctor ψ).map (d j i) ≫ h j =
    (relativeRecoveryFunctor ψ).map (d i j) ≫ h i)
omit [∀ i : 𝒰.I₀, Mono (h i)] in
include hrec in
Lean source · statement
theorem relativeRecoveredTripleTransition_chartMap (i j k : 𝒰.I₀) :
    (relativeRecoveryFunctor ψ).map (relativeTripleTransition 𝒰 A V d y ℓ hV t ht i j k) ≫
      (relativeRecoveryFunctor ψ).map (pullback.fst _ _) ≫
        (relativeRecoveryFunctor ψ).map (d j k) ≫ h j =
    (relativeRecoveryFunctor ψ).map (pullback.fst _ _) ≫
      (relativeRecoveryFunctor ψ).map (d i j) ≫ h i
theorem

relativeRecoveredTripleTransition_cocycle

L159 ↗
AlgebraicGeometry.Scheme.Cover.relativeRecoveredTripleTransition_cocycle
Documentation

The actual triple cocycle holds after recovering the local charts. This is the equation to descend eventually, not an assumption of faithful pullback at the current stage.

Source context 17 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace AlgebraicGeometry.Scheme.Cover
variable {B S : 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' Z : Scheme.{u}} (ψ : B' ⟶ B)
variable (h : ∀ i : 𝒰.I₀, (relativeRecoveryFunctor ψ).obj (A i) ⟶ Z)
variable [∀ i : 𝒰.I₀, Mono (h i)]
variable (hrec : ∀ i j : 𝒰.I₀,
  (relativeRecoveryFunctor ψ).map (t i j) ≫
      (relativeRecoveryFunctor ψ).map (d j i) ≫ h j =
    (relativeRecoveryFunctor ψ).map (d i j) ≫ h i)
include hV hrec in
Lean source · statement
theorem relativeRecoveredTripleTransition_cocycle (i j k : 𝒰.I₀) :
    (relativeRecoveryFunctor ψ).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) =
      (relativeRecoveryFunctor ψ).map (𝟙 (relativeTriple 𝒰 A V d i j k))

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