NYLL
Module

RelativeChartBaseChange.lean

Nyll.SchemeTheory.Gluing.RelativeChartBaseChange
9 declarations indexed from sourceView source ↗

Module documentation

Actual relative chart data after a base change

Base change of local models and their actual overlaps retains the chart structure morphisms, finite-etaleness, and cartesian overlap squares. Any transition morphism over the new base then preserves the second chart structure map, with no faithful-base-change assumption.

Imports3
Imported by2

Declarations

def

relativeChartStructure

L38 ↗
AlgebraicGeometry.Scheme.Cover.relativeChartStructure
Documentation

The actual local structural morphism regarded as a map over the ambient base.

Source context 12 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
variable {S T : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over S) (V : 𝒰.I₀ × 𝒰.I₀ → Over S)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (hy : ∀ i : 𝒰.I₀, y i ≫ 𝒰.f i = (A i).hom)
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 hy in
Lean source · statement
def relativeChartStructure (i : 𝒰.I₀) : A i ⟶ gluingChartOver 𝒰 i
def

relativeChartOverlapSecond

L43 ↗
AlgebraicGeometry.Scheme.Cover.relativeChartOverlapSecond
Documentation

The second projection from an actual overlap, regarded as a map over the base.

Source context 12 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
variable {S T : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over S) (V : 𝒰.I₀ × 𝒰.I₀ → Over S)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (hy : ∀ i : 𝒰.I₀, y i ≫ 𝒰.f i = (A i).hom)
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 hy hV in
Lean source · statement
def relativeChartOverlapSecond (i j : 𝒰.I₀) : V (i, j) ⟶ gluingChartOver 𝒰 j
def

relativeBaseChangedChartStructure

L53 ↗
AlgebraicGeometry.Scheme.Cover.relativeBaseChangedChartStructure
Documentation

The actual base-changed local structural map to the base-changed chart.

Source context 13 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
variable {S T : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over S) (V : 𝒰.I₀ × 𝒰.I₀ → Over S)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (hy : ∀ i : 𝒰.I₀, y i ≫ 𝒰.f i = (A i).hom)
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 ⟶ S)
include hy in
Lean source · statement
def relativeBaseChangedChartStructure (i : 𝒰.I₀) :
    ((Over.pullback φ).obj (A i)).left ⟶ (swappedPullbackCover φ 𝒰).X i
def

relativeBaseChangedOverlapSecond

L59 ↗
AlgebraicGeometry.Scheme.Cover.relativeBaseChangedOverlapSecond
Documentation

The actual second projection of a base-changed overlap.

Source context 13 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
variable {S T : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over S) (V : 𝒰.I₀ × 𝒰.I₀ → Over S)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (hy : ∀ i : 𝒰.I₀, y i ≫ 𝒰.f i = (A i).hom)
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 ⟶ S)
include hy hV in
Lean source · statement
def relativeBaseChangedOverlapSecond (i j : 𝒰.I₀) :
    ((Over.pullback φ).obj (V (i, j))).left ⟶ (swappedPullbackCover φ 𝒰).X j
theorem

relativeBaseChangedChartStructure_base

L64 ↗
AlgebraicGeometry.Scheme.Cover.relativeBaseChangedChartStructure_base
Documentation

Base-changed local maps have their literal ambient structural morphism.

Source context 12 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
variable {S T : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over S) (V : 𝒰.I₀ × 𝒰.I₀ → Over S)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (hy : ∀ i : 𝒰.I₀, y i ≫ 𝒰.f i = (A i).hom)
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 ⟶ S)
Lean source · statement
theorem relativeBaseChangedChartStructure_base (i : 𝒰.I₀) :
    relativeBaseChangedChartStructure 𝒰 A y hy φ i ≫ (swappedPullbackCover φ 𝒰).f i =
      ((Over.pullback φ).obj (A i)).hom
theorem

relativeBaseChangedChartStructure_finiteEtale

L70 ↗
AlgebraicGeometry.Scheme.Cover.relativeBaseChangedChartStructure_finiteEtale
Documentation

Base change preserves finite-etaleness of the actual local chart map.

Source context 12 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
variable {S T : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over S) (V : 𝒰.I₀ × 𝒰.I₀ → Over S)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (hy : ∀ i : 𝒰.I₀, y i ≫ 𝒰.f i = (A i).hom)
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 ⟶ S)
Lean source · statement
theorem relativeBaseChangedChartStructure_finiteEtale
    [∀ i : 𝒰.I₀, IsFiniteEtale (y i)] (i : 𝒰.I₀) :
    IsFiniteEtale (relativeBaseChangedChartStructure 𝒰 A y hy φ i)
theorem

relativeBaseChangedOverlap_isPullback

L79 ↗
AlgebraicGeometry.Scheme.Cover.relativeBaseChangedOverlap_isPullback
Documentation

Cartesian pairwise overlaps remain the actual cartesian overlaps over the base-changed open charts.

Source context 12 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
variable {S T : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over S) (V : 𝒰.I₀ × 𝒰.I₀ → Over S)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (hy : ∀ i : 𝒰.I₀, y i ≫ 𝒰.f i = (A i).hom)
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 ⟶ S)
Lean source · statement
theorem relativeBaseChangedOverlap_isPullback (i j : 𝒰.I₀) :
    IsPullback ((Over.pullback φ).map (d i j)).left
      (relativeBaseChangedOverlapSecond 𝒰 A V d y hy ℓ hV φ i j)
      (relativeBaseChangedChartStructure 𝒰 A y hy φ i ≫ (swappedPullbackCover φ 𝒰).f i)
      ((swappedPullbackCover φ 𝒰).f j)
theorem

relativeBaseChangedTransition_structure

L96 ↗
AlgebraicGeometry.Scheme.Cover.relativeBaseChangedTransition_structure
Documentation

Any transition over the new ambient base preserves the second chart structural map because open chart maps are monomorphisms.

Source context 12 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
variable {S T : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over S) (V : 𝒰.I₀ × 𝒰.I₀ → Over S)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (hy : ∀ i : 𝒰.I₀, y i ≫ 𝒰.f i = (A i).hom)
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 ⟶ S)
Lean source · statement
theorem relativeBaseChangedTransition_structure
    (t : ∀ i j : 𝒰.I₀,
      (Over.pullback φ).obj (V (i, j)) ⟶ (Over.pullback φ).obj (V (j, i)))
    (i j : 𝒰.I₀) :
    (t i j).left ≫ ((Over.pullback φ).map (d j i)).left ≫
        relativeBaseChangedChartStructure 𝒰 A y hy φ j =
      relativeBaseChangedOverlapSecond 𝒰 A V d y hy ℓ hV φ i j
theorem

relativeBaseChangedChart_compactSpace

L113 ↗
AlgebraicGeometry.Scheme.Cover.relativeBaseChangedChart_compactSpace
Documentation

Quasi-compact base change preserves compactness of the actual open chart.

Source context 12 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
variable {S T : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over S) (V : 𝒰.I₀ × 𝒰.I₀ → Over S)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (hy : ∀ i : 𝒰.I₀, y i ≫ 𝒰.f i = (A i).hom)
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 ⟶ S)
Lean source · statement
theorem relativeBaseChangedChart_compactSpace [QuasiCompact φ]
    (i : 𝒰.I₀) [CompactSpace (𝒰.X i)] :
    CompactSpace ((swappedPullbackCover φ 𝒰).X i)

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