NYLL
Module

Scheme_Modules_IsInvertible_exists_isAffineOpen_isFrameOn_preimage_of_isDirectLimit.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_isAffineOpen_isFrameOn_preimage_of_isDirectLimit
71 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Is Invertible exists is Affine Open is Frame On preimage of is Direct Limit

Imports29
  • Mathlib.Algebra.Category.Ring.Basic
  • Mathlib.Algebra.Category.Ring.FilteredColimits
  • Mathlib.Algebra.Colimit.Module
  • Mathlib.AlgebraicGeometry.AffineScheme
  • Mathlib.AlgebraicGeometry.AffineTransitionLimit
  • Mathlib.AlgebraicGeometry.GammaSpecAdjunction
  • Mathlib.AlgebraicGeometry.Modules.Sheaf
  • Mathlib.AlgebraicGeometry.Morphisms.Affine
  • Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
  • Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
  • Mathlib.CategoryTheory.Adjunction.Limits
  • Mathlib.CategoryTheory.Filtered.Basic
  • Mathlib.CategoryTheory.Filtered.Connected
  • Mathlib.CategoryTheory.IsConnected
  • Mathlib.CategoryTheory.Limits.Opposites
  • Mathlib.CategoryTheory.Limits.Preserves.Basic
  • Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
  • Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  • Mathlib.CategoryTheory.Limits.Types.Filtered
  • Mathlib.CategoryTheory.MorphismProperty.Limits
  • Mathlib.Data.Fintype.EquivFin
  • Mathlib.Topology.Sets.OpenCover
  • Mathlib.Topology.Sets.Opens
  • Mathlib.Tactic.Convert
  • Mathlib.Tactic.Simps.Basic
  • Nyll.AlgebraicCurves.Foundations.Algebra.Mathlib_Algebra_IsDirectLimit
  • Nyll.SchemeTheory.Modules.TensorSections
  • Nyll.AlgebraicCurves.Geometry.Picard.Functor
  • Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_isFrameOn
Imported by2

Declarations

theorem

φ_self

L71 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.φ_self
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Ring
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
Lean source · statement
theorem φ_self (j : κ) : φ j j le_rfl = RingHom.id (G j)
theorem

φ_comp

L74 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.φ_comp
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Ring
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
Lean source · statement
theorem φ_comp {j k l : κ} (hjk : j ≤ k) (hkl : k ≤ l) : (φ k l hkl).comp (φ j k hjk) = φ j l
  (hjk.trans hkl)
def

ringDiag

L79 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.ringDiag
Documentation

The diagram of commutative rings underlying the directed system.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Ring
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
Lean source · full declaration
def ringDiag : κ ⥤ CommRingCat.{u} where
  obj j := CommRingCat.of (G j)
  map {j k} h := CommRingCat.ofHom (φ j k (leOfHom h))
  map_id j := by rw [← CommRingCat.ofHom_id]; congr 1; exact φ_self φ j
  map_comp {j k l} h h' := by rw [← CommRingCat.ofHom_comp]; congr 1; exact (φ_comp φ _ _).symm
def

ringCocone

L86 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.ringCocone
Documentation

The cocone of structure maps from the directed system to the limit ring.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Ring
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
Lean source · full declaration
def ringCocone (hRc : ∀ i j hij x, g j (φ i j hij x) = g i x) : Cocone (ringDiag φ) where
  pt := CommRingCat.of R
  ι := { app := fun j => CommRingCat.ofHom (g j)
         naturality := fun {j k} h => by
           apply CommRingCat.hom_ext; ext x
           change g k (φ j k (leOfHom h) x) = g j x
           exact hRc j k (leOfHom h) x }
def

specDiag

L95 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.specDiag
Documentation

The inverse diagram of affine schemes obtained by taking spectra.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Ring
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
Lean source · statement
def specDiag : κᵒᵖ ⥤ Scheme.{u}
theorem

specDiag_obj

L97 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.specDiag_obj
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Ring
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
Lean source · statement
theorem specDiag_obj (j : κᵒᵖ) : (specDiag φ).obj j = Spec (CommRingCat.of (G j.unop))
theorem

specDiag_map

L99 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.specDiag_map
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Ring
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
Lean source · statement
theorem specDiag_map {j k : κᵒᵖ} (h : j ⟶ k) :
    (specDiag φ).map h = Spec.map (CommRingCat.ofHom (φ k.unop j.unop (leOfHom h.unop)))
instance

isAffine_specDiag_obj

L102 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.isAffine_specDiag_obj
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Ring
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
Lean source · statement
instance isAffine_specDiag_obj (j : κᵒᵖ) : IsAffine ((specDiag φ).obj j)
instance

isAffineHom_specDiag_map

L105 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.isAffineHom_specDiag_map
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Ring
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
Lean source · statement
instance isAffineHom_specDiag_map {j k : κᵒᵖ} (h : j ⟶ k) : IsAffineHom ((specDiag φ).map h)
def

isColimitRingCocone

L113 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.isColimitRingCocone
Documentation

The colimit structure on the ring cocone supplied by the direct-limit property.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Ring
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [Nonempty κ] [IsDirectedOrder κ] (hR : IsDirectLimit (fun j k h => ⇑(φ j k h)) fun j =>
  ⇑(g j))
Lean source · statement
def isColimitRingCocone : IsColimit (ringCocone φ g hR.compatibility)
def

specCone

L126 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.specCone
Documentation

The cone on the spectra diagram induced by the ring cocone.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Ring
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [Nonempty κ] [IsDirectedOrder κ] (hR : IsDirectLimit (fun j k h => ⇑(φ j k h)) fun j =>
  ⇑(g j))
Lean source · statement
def specCone : Cone (specDiag φ)
theorem

specCone_pt

L130 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.specCone_pt
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Ring
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [Nonempty κ] [IsDirectedOrder κ] (hR : IsDirectLimit (fun j k h => ⇑(φ j k h)) fun j =>
  ⇑(g j))
omit [Nonempty κ] [IsDirectedOrder κ] in
Lean source · statement
theorem specCone_pt : (specCone φ g hR).pt = Spec (CommRingCat.of R)
theorem

specCone_π

L133 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.specCone_π
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Ring
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [Nonempty κ] [IsDirectedOrder κ] (hR : IsDirectLimit (fun j k h => ⇑(φ j k h)) fun j =>
  ⇑(g j))
omit [Nonempty κ] [IsDirectedOrder κ] in
Lean source · statement
theorem specCone_π (j : κᵒᵖ) : (specCone φ g hR).π.app j = Spec.map (CommRingCat.ofHom (g j.unop))
def

isLimitSpecCone

L137 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.isLimitSpecCone
Documentation

The limit structure on the spectra cone, transported from the ring colimit.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Ring
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [Nonempty κ] [IsDirectedOrder κ] (hR : IsDirectLimit (fun j k h => ⇑(φ j k h)) fun j =>
  ⇑(g j))
Lean source · statement
def isLimitSpecCone : IsLimit (specCone φ g hR)
abbrev

sφ

L151 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.sφ
Documentation

The morphism of spectra induced by a transition ring homomorphism.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
Lean source · statement
abbrev sφ {j k : κ} (h : j ≤ k) : Spec (CommRingCat.of (G k)) ⟶ Spec (CommRingCat.of
  (G j))
abbrev

sg

L156 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.sg
Documentation

The morphism of spectra induced by a structure map into the limit ring.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
Lean source · statement
abbrev sg (j : κ) : Spec (CommRingCat.of R) ⟶ Spec (CommRingCat.of (G j))
theorem

sφ_irrel

L159 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.sφ_irrel
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
Lean source · statement
theorem sφ_irrel {j k : κ} (h h' : j ≤ k) : sφ φ h = sφ φ h'
theorem

sg_comp

L161 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.sg_comp
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
Lean source · statement
theorem sg_comp (hRc : ∀ i j hij x, g j (φ i j hij x) = g i x) {j k : κ} (hjk : j ≤ k) :
    sg g k ≫ sφ φ hjk = sg g j
theorem

sφ_comp

L169 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.sφ_comp
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
Lean source · statement
theorem sφ_comp {j k l : κ} (hjk : j ≤ k) (hkl : k ≤ l) : sφ φ hkl ≫ sφ φ hjk = sφ φ (hjk.trans
  hkl)
theorem

sφ_self

L173 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.sφ_self
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
Lean source · statement
theorem sφ_self (j : κ) : sφ φ (le_refl j) = 𝟙 _
def

D

L182 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.D
Documentation

The diagram formed by base changing the scheme to the rings of the directed system.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
variable (b : κ) (hb : ∀ j, b ≤ j) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G b)))
Lean source · full declaration
def D : κᵒᵖ ⥤ Scheme.{u} where
  obj j := pullback fX (sφ φ (hb j.unop))
  map {j k} f := pullback.map fX (sφ φ (hb j.unop)) fX (sφ φ (hb k.unop)) (𝟙 X) (sφ φ (leOfHom
    f.unop)) (𝟙 _)
      (by rw [Category.comp_id, Category.id_comp]) (by rw [Category.comp_id, sφ_comp])
  map_id j := by
    apply pullback.hom_ext
    · rw [pullback.lift_fst, Category.id_comp, Category.comp_id]
    · rw [pullback.lift_snd, Category.id_comp]
      convert Category.comp_id _
      exact sφ_self φ _
  map_comp {j k l} f f' := by
    apply pullback.hom_ext
    · simp only [pullback.lift_fst, Category.assoc, Category.comp_id]
    · simp only [pullback.lift_snd, Category.assoc, pullback.lift_snd_assoc]
      rw [sφ_comp]
def

t

L200 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.t
Documentation

The natural transformation from the base-change diagram to the fixed base spectrum.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
variable (b : κ) (hb : ∀ j, b ≤ j) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G b)))
Lean source · full declaration
def t : D φ b hb fX ⟶ (Functor.const _).obj (Spec (CommRingCat.of (G b))) where
  app j := pullback.fst fX (sφ φ (hb j.unop)) ≫ fX
  naturality {j k} f := by
    simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.comp_id, D]
    rw [← Category.assoc, pullback.lift_fst, Category.comp_id]
theorem

D_obj

L206 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.D_obj
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
variable (b : κ) (hb : ∀ j, b ≤ j) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G b)))
Lean source · statement
theorem D_obj (j : κᵒᵖ) : (D φ b hb fX).obj j = pullback fX (sφ φ (hb j.unop))
theorem

D_map_fst

L208 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.D_map_fst
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
variable (b : κ) (hb : ∀ j, b ≤ j) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G b)))
Lean source · statement
theorem D_map_fst {j k : κᵒᵖ} (f : j ⟶ k) :
    (D φ b hb fX).map f ≫ pullback.fst fX (sφ φ (hb k.unop)) = pullback.fst fX (sφ φ (hb j.unop))
theorem

D_map_snd

L212 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.D_map_snd
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
variable (b : κ) (hb : ∀ j, b ≤ j) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G b)))
Lean source · statement
theorem D_map_snd {j k : κᵒᵖ} (f : j ⟶ k) :
    (D φ b hb fX).map f ≫ pullback.snd fX (sφ φ (hb k.unop)) =
      pullback.snd fX (sφ φ (hb j.unop)) ≫ sφ φ (leOfHom f.unop)
theorem

t_app

L217 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.t_app
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
variable (b : κ) (hb : ∀ j, b ≤ j) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G b)))
Lean source · statement
theorem t_app (j : κᵒᵖ) : (t φ b hb fX).app j = pullback.fst fX (sφ φ (hb j.unop)) ≫ fX
theorem

isPullback_D_map

L219 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.isPullback_D_map
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
variable (b : κ) (hb : ∀ j, b ≤ j) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G b)))
Lean source · statement
theorem isPullback_D_map {j k : κᵒᵖ} (f : j ⟶ k) :
    IsPullback ((D φ b hb fX).map f) (pullback.snd fX (sφ φ (hb j.unop))) (pullback.snd fX (sφ φ
      (hb k.unop)))
      (sφ φ (leOfHom f.unop))
instance

isAffineHom_D_map

L229 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.isAffineHom_D_map
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
variable (b : κ) (hb : ∀ j, b ≤ j) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G b)))
Lean source · statement
instance isAffineHom_D_map {j k : κᵒᵖ} (f : j ⟶ k) : IsAffineHom ((D φ b hb fX).map f)
instance

compactSpace_pullback_sφ

L233 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.compactSpace_pullback_sφ
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
variable (b : κ) (hb : ∀ j, b ≤ j) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G b)))
Lean source · statement
instance compactSpace_pullback_sφ [CompactSpace X] (j : κ) : CompactSpace ↥(pullback fX (sφ
  φ (hb j)))
instance

compactSpace_D_obj

L239 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.compactSpace_D_obj
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
variable (b : κ) (hb : ∀ j, b ≤ j) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G b)))
Lean source · statement
instance compactSpace_D_obj [CompactSpace X] (j : κᵒᵖ) : CompactSpace ((D φ b hb fX).obj j)
instance

quasiSeparatedSpace_pullback_sφ

L243 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.quasiSeparatedSpace_pullback_sφ
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
variable (b : κ) (hb : ∀ j, b ≤ j) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G b)))
Lean source · statement
instance quasiSeparatedSpace_pullback_sφ [QuasiSeparatedSpace X] (j : κ) :
    QuasiSeparatedSpace ↥(pullback fX (sφ φ (hb j)))
instance

quasiSeparatedSpace_D_obj

L248 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.quasiSeparatedSpace_D_obj
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
variable (b : κ) (hb : ∀ j, b ≤ j) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G b)))
Lean source · statement
instance quasiSeparatedSpace_D_obj [QuasiSeparatedSpace X] (j : κᵒᵖ) : QuasiSeparatedSpace
  ((D φ b hb fX).obj j)
def

α

L253 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.α
Documentation

The projection from the base-change diagram to the spectra diagram.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
variable (b : κ) (hb : ∀ j, b ≤ j) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G b)))
Lean source · full declaration
def α : D φ b hb fX ⟶ specDiag φ where
  app j := pullback.snd fX (sφ φ (hb j.unop))
  naturality {_ _} f := D_map_snd φ b hb fX f
def

c

L262 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.c
Documentation

The cone from base change to the limit ring over the stage base-change diagram.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
variable (b : κ) (hb : ∀ j, b ≤ j) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G b)))
section Cone
variable (hRc : ∀ i j hij x, g j (φ i j hij x) = g i x)
Lean source · full declaration
def c : Cone (D φ b hb fX) where
  pt := pullback fX (sg g b)
  π :=
    { app := fun j => pullback.map fX (sg g b) fX (sφ φ (hb j.unop)) (𝟙 X) (sg g j.unop) (𝟙 _)
          (by rw [Category.comp_id, Category.id_comp]) (by rw [Category.comp_id, sg_comp φ g hRc])
      naturality := by
        intro j k f
        simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.id_comp, D]
        apply pullback.hom_ext
        · simp only [Category.assoc, pullback.lift_fst, Category.comp_id]
        · simp only [Category.assoc, pullback.lift_snd, pullback.lift_snd_assoc]
          rw [sg_comp φ g hRc] }
theorem

c_pt

L275 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.c_pt
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
variable (b : κ) (hb : ∀ j, b ≤ j) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G b)))
section Cone
variable (hRc : ∀ i j hij x, g j (φ i j hij x) = g i x)
Lean source · statement
theorem c_pt : (c φ g b hb fX hRc).pt = pullback fX (sg g b)
theorem

c_π_fst

L277 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.c_π_fst
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
variable (b : κ) (hb : ∀ j, b ≤ j) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G b)))
section Cone
variable (hRc : ∀ i j hij x, g j (φ i j hij x) = g i x)
Lean source · statement
theorem c_π_fst (j : κᵒᵖ) :
    (c φ g b hb fX hRc).π.app j ≫ pullback.fst fX (sφ φ (hb j.unop)) = pullback.fst fX (sg g b)
theorem

c_π_snd

L281 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.c_π_snd
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
variable (b : κ) (hb : ∀ j, b ≤ j) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G b)))
section Cone
variable (hRc : ∀ i j hij x, g j (φ i j hij x) = g i x)
Lean source · statement
theorem c_π_snd (j : κᵒᵖ) :
    (c φ g b hb fX hRc).π.app j ≫ pullback.snd fX (sφ φ (hb j.unop)) = pullback.snd fX (sg g b) ≫
      sg g j.unop
theorem

isPullback_c_π

L286 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.isPullback_c_π
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
variable (b : κ) (hb : ∀ j, b ≤ j) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G b)))
section Cone
variable (hRc : ∀ i j hij x, g j (φ i j hij x) = g i x)
Lean source · statement
theorem isPullback_c_π (j : κᵒᵖ) :
    IsPullback ((c φ g b hb fX hRc).π.app j) (pullback.snd fX (sg g b)) (pullback.snd fX (sφ φ (hb
      j.unop)))
      (sg g j.unop)
def

isLimitCone

L302 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.isLimitCone
Documentation

The limit structure on the base-change cone.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section BaseChange
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
variable [DirectedSystem G fun j k h => ⇑(φ j k h)]
variable (b : κ) (hb : ∀ j, b ≤ j) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G b)))
variable [Nonempty κ] [IsDirectedOrder κ] (hR : IsDirectLimit (fun j k h => ⇑(φ j k h)) fun j =>
  ⇑(g j))
Lean source · statement
def isLimitCone : IsLimit (c φ g b hb fX hR.compatibility)
def

proj

L323 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.proj
Documentation

The projection from the limit base change to a specified stage.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section API
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] {φ : ∀ j k : κ, j ≤ k → G j →+* G k}
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] {g : ∀ j, G j →+* R}
  {b : κ} {hb : ∀ j, b ≤ j} {X : Scheme.{u}} {fX : X ⟶ Spec (CommRingCat.of (G b))}
  {hRc : ∀ i j hij x, g j (φ i j hij x) = g i x}
Lean source · full declaration
def proj (φ : ∀ j k : κ, j ≤ k → G j →+* G k) [DirectedSystem G fun j k h => ⇑(φ j k
  h)]
    (g : ∀ j, G j →+* R) (hb : ∀ j, b ≤ j)
    (fX : X ⟶ Spec (CommRingCat.of (G b))) (hRc : ∀ i j hij x, g j (φ i j hij x) = g i x) (j : κ) :
    pullback fX (sg g b) ⟶ (D φ b hb fX).obj (op j) :=
  (c φ g b hb fX hRc).π.app (op j)
def

fstL

L331 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.fstL
Documentation

The projection of a stage base change to the original scheme.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section API
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] {φ : ∀ j k : κ, j ≤ k → G j →+* G k}
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] {g : ∀ j, G j →+* R}
  {b : κ} {hb : ∀ j, b ≤ j} {X : Scheme.{u}} {fX : X ⟶ Spec (CommRingCat.of (G b))}
  {hRc : ∀ i j hij x, g j (φ i j hij x) = g i x}
Lean source · full declaration
def fstL (φ : ∀ j k : κ, j ≤ k → G j →+* G k) [DirectedSystem G fun j k h => ⇑(φ j k
  h)]
    (hb : ∀ j, b ≤ j) (fX : X ⟶ Spec (CommRingCat.of (G b))) (j : κ) : (D φ b hb fX).obj (op j) ⟶ X
      :=
  pullback.fst fX (sφ φ (hb j))
def

sndL

L338 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.sndL
Documentation

The projection of a stage base change to its base spectrum.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section API
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] {φ : ∀ j k : κ, j ≤ k → G j →+* G k}
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] {g : ∀ j, G j →+* R}
  {b : κ} {hb : ∀ j, b ≤ j} {X : Scheme.{u}} {fX : X ⟶ Spec (CommRingCat.of (G b))}
  {hRc : ∀ i j hij x, g j (φ i j hij x) = g i x}
Lean source · full declaration
def sndL (φ : ∀ j k : κ, j ≤ k → G j →+* G k) [DirectedSystem G fun j k h => ⇑(φ j k
  h)]
    (hb : ∀ j, b ≤ j) (fX : X ⟶ Spec (CommRingCat.of (G b))) (j : κ) :
    (D φ b hb fX).obj (op j) ⟶ Spec (CommRingCat.of (G j)) :=
  pullback.snd fX (sφ φ (hb j))
theorem

proj_def

L344 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.proj_def
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section API
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] {φ : ∀ j k : κ, j ≤ k → G j →+* G k}
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] {g : ∀ j, G j →+* R}
  {b : κ} {hb : ∀ j, b ≤ j} {X : Scheme.{u}} {fX : X ⟶ Spec (CommRingCat.of (G b))}
  {hRc : ∀ i j hij x, g j (φ i j hij x) = g i x}
Lean source · statement
theorem proj_def (j : κ) : (c φ g b hb fX hRc).π.app (op j) = proj φ g hb fX hRc j
theorem

fstL_def

L345 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.fstL_def
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section API
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] {φ : ∀ j k : κ, j ≤ k → G j →+* G k}
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] {g : ∀ j, G j →+* R}
  {b : κ} {hb : ∀ j, b ≤ j} {X : Scheme.{u}} {fX : X ⟶ Spec (CommRingCat.of (G b))}
  {hRc : ∀ i j hij x, g j (φ i j hij x) = g i x}
Lean source · statement
theorem fstL_def (j : κ) : pullback.fst fX (sφ φ (hb j)) = fstL φ hb fX j
theorem

sndL_def

L346 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.sndL_def
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section API
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] {φ : ∀ j k : κ, j ≤ k → G j →+* G k}
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] {g : ∀ j, G j →+* R}
  {b : κ} {hb : ∀ j, b ≤ j} {X : Scheme.{u}} {fX : X ⟶ Spec (CommRingCat.of (G b))}
  {hRc : ∀ i j hij x, g j (φ i j hij x) = g i x}
Lean source · statement
theorem sndL_def (j : κ) : pullback.snd fX (sφ φ (hb j)) = sndL φ hb fX j
theorem

t_appL

L347 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.t_appL
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section API
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] {φ : ∀ j k : κ, j ≤ k → G j →+* G k}
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] {g : ∀ j, G j →+* R}
  {b : κ} {hb : ∀ j, b ≤ j} {X : Scheme.{u}} {fX : X ⟶ Spec (CommRingCat.of (G b))}
  {hRc : ∀ i j hij x, g j (φ i j hij x) = g i x}
Lean source · statement
theorem t_appL (j : κ) : (t φ b hb fX).app (op j) = fstL φ hb fX j ≫ fX
theorem

hom_extL

L349 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.hom_extL
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section API
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] {φ : ∀ j k : κ, j ≤ k → G j →+* G k}
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] {g : ∀ j, G j →+* R}
  {b : κ} {hb : ∀ j, b ≤ j} {X : Scheme.{u}} {fX : X ⟶ Spec (CommRingCat.of (G b))}
  {hRc : ∀ i j hij x, g j (φ i j hij x) = g i x}
Lean source · statement
theorem hom_extL {j : κ} {W : Scheme.{u}} {a a' : W ⟶ (D φ b hb fX).obj (op j)}
    (h₁ : a ≫ fstL φ hb fX j = a' ≫ fstL φ hb fX j) (h₂ : a ≫ sndL φ hb fX j = a' ≫ sndL φ hb fX j)
      : a = a'
theorem

conditionL

L354 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.conditionL
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section API
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] {φ : ∀ j k : κ, j ≤ k → G j →+* G k}
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] {g : ∀ j, G j →+* R}
  {b : κ} {hb : ∀ j, b ≤ j} {X : Scheme.{u}} {fX : X ⟶ Spec (CommRingCat.of (G b))}
  {hRc : ∀ i j hij x, g j (φ i j hij x) = g i x}
Lean source · statement
theorem conditionL (j : κ) : fstL φ hb fX j ≫ fX = sndL φ hb fX j ≫ sφ φ (hb j)
def

liftL

L358 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.liftL
Documentation

The morphism into a stage base change induced by compatible projection maps.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section API
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] {φ : ∀ j k : κ, j ≤ k → G j →+* G k}
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] {g : ∀ j, G j →+* R}
  {b : κ} {hb : ∀ j, b ≤ j} {X : Scheme.{u}} {fX : X ⟶ Spec (CommRingCat.of (G b))}
  {hRc : ∀ i j hij x, g j (φ i j hij x) = g i x}
Lean source · full declaration
def liftL (φ : ∀ j k : κ, j ≤ k → G j →+* G k) [DirectedSystem G fun j k h => ⇑(φ j k
  h)]
    (hb : ∀ j, b ≤ j) (fX : X ⟶ Spec (CommRingCat.of (G b))) (j : κ) {W : Scheme.{u}} (a : W ⟶ X)
    (a' : W ⟶ Spec (CommRingCat.of (G j))) (w : a ≫ fX = a' ≫ sφ φ (hb j)) : W ⟶ (D φ b hb fX).obj
      (op j) :=
  pullback.lift a a' w
theorem

liftL_fstL

L365 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.liftL_fstL
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section API
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] {φ : ∀ j k : κ, j ≤ k → G j →+* G k}
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] {g : ∀ j, G j →+* R}
  {b : κ} {hb : ∀ j, b ≤ j} {X : Scheme.{u}} {fX : X ⟶ Spec (CommRingCat.of (G b))}
  {hRc : ∀ i j hij x, g j (φ i j hij x) = g i x}
Lean source · statement
theorem liftL_fstL (j : κ) {W : Scheme.{u}} (a : W ⟶ X) (a' : W ⟶ Spec (CommRingCat.of (G j)))
    (w : a ≫ fX = a' ≫ sφ φ (hb j)) : liftL φ hb fX j a a' w ≫ fstL φ hb fX j = a
theorem

liftL_sndL

L369 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.liftL_sndL
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section API
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] {φ : ∀ j k : κ, j ≤ k → G j →+* G k}
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] {g : ∀ j, G j →+* R}
  {b : κ} {hb : ∀ j, b ≤ j} {X : Scheme.{u}} {fX : X ⟶ Spec (CommRingCat.of (G b))}
  {hRc : ∀ i j hij x, g j (φ i j hij x) = g i x}
Lean source · statement
theorem liftL_sndL (j : κ) {W : Scheme.{u}} (a : W ⟶ X) (a' : W ⟶ Spec (CommRingCat.of (G j)))
    (w : a ≫ fX = a' ≫ sφ φ (hb j)) : liftL φ hb fX j a a' w ≫ sndL φ hb fX j = a'
theorem

D_map_eq

L373 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.D_map_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section API
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] {φ : ∀ j k : κ, j ≤ k → G j →+* G k}
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] {g : ∀ j, G j →+* R}
  {b : κ} {hb : ∀ j, b ≤ j} {X : Scheme.{u}} {fX : X ⟶ Spec (CommRingCat.of (G b))}
  {hRc : ∀ i j hij x, g j (φ i j hij x) = g i x}
Lean source · statement
theorem D_map_eq {j j' : κ} (f f' : (op j' : κᵒᵖ) ⟶ op j) : (D φ b hb fX).map f = (D φ b hb fX).map
  f'
theorem

D_map_fstL

L377 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.D_map_fstL
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section API
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] {φ : ∀ j k : κ, j ≤ k → G j →+* G k}
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] {g : ∀ j, G j →+* R}
  {b : κ} {hb : ∀ j, b ≤ j} {X : Scheme.{u}} {fX : X ⟶ Spec (CommRingCat.of (G b))}
  {hRc : ∀ i j hij x, g j (φ i j hij x) = g i x}
Lean source · statement
theorem D_map_fstL {j j' : κ} (f : (op j' : κᵒᵖ) ⟶ op j) : (D φ b hb fX).map f ≫ fstL φ hb fX j =
  fstL φ hb fX j'
theorem

D_map_sndL

L381 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.D_map_sndL
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section API
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] {φ : ∀ j k : κ, j ≤ k → G j →+* G k}
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] {g : ∀ j, G j →+* R}
  {b : κ} {hb : ∀ j, b ≤ j} {X : Scheme.{u}} {fX : X ⟶ Spec (CommRingCat.of (G b))}
  {hRc : ∀ i j hij x, g j (φ i j hij x) = g i x}
Lean source · statement
theorem D_map_sndL {j j' : κ} (f : (op j' : κᵒᵖ) ⟶ op j) :
    (D φ b hb fX).map f ≫ sndL φ hb fX j = sndL φ hb fX j' ≫ sφ φ (leOfHom f.unop)
theorem

D_map_map

L385 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.D_map_map
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section API
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] {φ : ∀ j k : κ, j ≤ k → G j →+* G k}
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] {g : ∀ j, G j →+* R}
  {b : κ} {hb : ∀ j, b ≤ j} {X : Scheme.{u}} {fX : X ⟶ Spec (CommRingCat.of (G b))}
  {hRc : ∀ i j hij x, g j (φ i j hij x) = g i x}
Lean source · statement
theorem D_map_map {j j' j'' : κ} (f : (op j' : κᵒᵖ) ⟶ op j) (f' : (op j'' : κᵒᵖ) ⟶ op j') (f'' :
  (op j'' : κᵒᵖ) ⟶ op j) :
    (D φ b hb fX).map f' ≫ (D φ b hb fX).map f = (D φ b hb fX).map f''
theorem

proj_map

L390 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.proj_map
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section API
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] {φ : ∀ j k : κ, j ≤ k → G j →+* G k}
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] {g : ∀ j, G j →+* R}
  {b : κ} {hb : ∀ j, b ≤ j} {X : Scheme.{u}} {fX : X ⟶ Spec (CommRingCat.of (G b))}
  {hRc : ∀ i j hij x, g j (φ i j hij x) = g i x}
Lean source · statement
theorem proj_map {j j' : κ} (f : (op j' : κᵒᵖ) ⟶ op j) : proj φ g hb fX hRc j' ≫ (D φ b hb fX).map
  f = proj φ g hb fX hRc j
theorem

proj_fstL

L394 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.proj_fstL
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section API
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] {φ : ∀ j k : κ, j ≤ k → G j →+* G k}
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] {g : ∀ j, G j →+* R}
  {b : κ} {hb : ∀ j, b ≤ j} {X : Scheme.{u}} {fX : X ⟶ Spec (CommRingCat.of (G b))}
  {hRc : ∀ i j hij x, g j (φ i j hij x) = g i x}
Lean source · statement
theorem proj_fstL (j : κ) : proj φ g hb fX hRc j ≫ fstL φ hb fX j = pullback.fst fX (sg g b)
theorem

proj_sndL

L397 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.proj_sndL
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section API
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] {φ : ∀ j k : κ, j ≤ k → G j →+* G k}
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] {g : ∀ j, G j →+* R}
  {b : κ} {hb : ∀ j, b ≤ j} {X : Scheme.{u}} {fX : X ⟶ Spec (CommRingCat.of (G b))}
  {hRc : ∀ i j hij x, g j (φ i j hij x) = g i x}
Lean source · statement
theorem proj_sndL (j : κ) : proj φ g hb fX hRc j ≫ sndL φ hb fX j = pullback.snd fX (sg g b) ≫ sg g
  j
def

homOp

L402 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.homOp
Documentation

The opposite-category morphism induced by an inequality of indices.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section API
variable {κ : Type u} [Preorder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] {φ : ∀ j k : κ, j ≤ k → G j →+* G k}
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] {g : ∀ j, G j →+* R}
  {b : κ} {hb : ∀ j, b ≤ j} {X : Scheme.{u}} {fX : X ⟶ Spec (CommRingCat.of (G b))}
  {hRc : ∀ i j hij x, g j (φ i j hij x) = g i x}
Lean source · statement
def homOp {j j' : κ} (h : j ≤ j') : (op j' : κᵒᵖ) ⟶ op j
theorem

exists_open_core

L416 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.exists_open_core
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Core
variable {κ : Type u} [Preorder κ] [Nonempty κ] [IsDirectedOrder κ]
  {G : κ → Type u} [∀ j, CommRing (G j)] (φ : ∀ j k : κ, j ≤ k → G j →+* G k)
  [DirectedSystem G fun j k h => ⇑(φ j k h)]
  {R : Type u} [CommRing R] (g : ∀ j, G j →+* R)
  (hR : IsDirectLimit (fun j k h => ⇑(φ j k h)) fun j => ⇑(g j))
  (b : κ) (hb : ∀ j, b ≤ j)
include hR in
Lean source · statement
theorem exists_open_core {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G b)))
    (U : (pullback fX (sg g b)).Opens) (hU : IsCompact (U : Set ↥(pullback fX (sg g b)))) :
    ∃ (j : κ) (V : ((D φ b hb fX).obj (op j)).Opens),
      IsCompact (V : Set ↥((D φ b hb fX).obj (op j))) ∧ proj φ g hb fX hR.compatibility j ⁻¹ᵁ V = U
abbrev

J

L435 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.J
Documentation

The indices of the directed system lying above a fixed stage.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Reindex
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R) (i : ι)
Lean source · statement
abbrev J (i : ι) : Type u
abbrev

φ'

L438 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.φ'
Documentation

The transition homomorphisms on the subsystem above the fixed stage.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Reindex
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R) (i : ι)
Lean source · statement
abbrev φ' (j k : J i) (h : j ≤ k) : G j.1 →+* G k.1
abbrev

g'

L441 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.g'
Documentation

The structure maps to the limit ring restricted to the upper subsystem.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Reindex
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R) (i : ι)
Lean source · statement
abbrev g' (j : J i) : G j.1 →+* R
abbrev

bot

L444 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.bot
Documentation

The least index of the subsystem above the fixed stage.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Reindex
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R) (i : ι)
Lean source · statement
abbrev bot : J i
theorem

bot_le

L446 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.bot_le
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Reindex
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R) (i : ι)
Lean source · statement
theorem bot_le (j : J i) : bot i ≤ j
instance

directedSystem'

L448 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.directedSystem'
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Reindex
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R) (i : ι)
Lean source · full declaration
instance directedSystem' [DirectedSystem G fun i j h => ⇑(φ i j h)] :
    DirectedSystem (fun j : J i => G j.1) fun j k h => ⇑(φ' φ i j k h) where
  map_self := fun _ x => DirectedSystem.map_self (f := fun i j h => ⇑(φ i j h)) x
  map_map := fun _ _ _ hjk hkl x => DirectedSystem.map_map (f := fun i j h => ⇑(φ i j h)) hjk hkl x
instance

nonempty'

L453 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.nonempty'
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Reindex
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R) (i : ι)
Lean source · statement
instance nonempty' : Nonempty (J i)
instance

isDirectedOrder'

L455 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.isDirectedOrder'
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Reindex
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R) (i : ι)
Lean source · statement
instance isDirectedOrder' [IsDirectedOrder ι] : IsDirectedOrder (J i)
theorem

isDirectLimit'

L460 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread.isDirectLimit'
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace DirLimSpread
section Reindex
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R) (i : ι)
Lean source · full declaration
theorem isDirectLimit' [DirectedSystem G fun i j h => ⇑(φ i j h)] [IsDirectedOrder ι]
    (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i)) :
    IsDirectLimit (fun j k h => ⇑(φ' φ i j k h)) fun j => ⇑(g' g i j) where
  surj x := by
    obtain ⟨l, xl, hx⟩ := hR.surj x
    obtain ⟨m, him, hlm⟩ := exists_ge_ge i l
    exact ⟨⟨m, him⟩, φ l m hlm xl, (hR.compatibility l m hlm xl).trans hx⟩
  inj j k xj xk h := by
    obtain ⟨m, hjm, hkm, e⟩ := hR.inj j.1 k.1 xj xk h
    exact ⟨⟨m, j.2.trans hjm⟩, hjm, hkm, e⟩
  compatibility j k h x := hR.compatibility j.1 k.1 h x
theorem

exists_isFrameOn_congr

L505 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.AlgebraicGeometry.Scheme.Modules.exists_isFrameOn_congr
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
attribute [local instance] DirLimSpread.isAffine_specDiag_obj
attribute [local instance] DirLimSpread.isAffineHom_specDiag_map
attribute [local instance] DirLimSpread.isAffineHom_D_map
attribute [local instance] DirLimSpread.compactSpace_pullback_sφ
attribute [local instance] DirLimSpread.compactSpace_D_obj
attribute [local instance] DirLimSpread.quasiSeparatedSpace_pullback_sφ
attribute [local instance] DirLimSpread.quasiSeparatedSpace_D_obj
attribute [local instance] DirLimSpread.directedSystem'
attribute [local instance] DirLimSpread.nonempty'
attribute [local instance] DirLimSpread.isDirectedOrder'
open scoped _root_.AlgebraicGeometry in
open scoped _root_.AlgebraicGeometry.Scheme in
open scoped _root_.AlgebraicGeometry.Scheme.Modules in
Lean source · statement
theorem AlgebraicGeometry.Scheme.Modules.exists_isFrameOn_congr {Y : Scheme.{u}} {M : Y.Modules}
    {U U' : Y.Opens} (h : U = U') (hU : ∃ s : Γ(M, U), Scheme.Modules.IsFrameOn s U) :
    ∃ s : Γ(M, U'), Scheme.Modules.IsFrameOn s U'
theorem

exists_isAffineOpen_isFrameOn_preimage_of_isDirectLimit

L536 ↗
AlgebraicGeometry.Scheme.Modules.IsInvertible.exists_isAffineOpen_isFrameOn_preimage_of_isDirectLimit
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicGeometry.Scheme.Modules.IsInvertible
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
attribute [local instance] DirLimSpread.isAffine_specDiag_obj
attribute [local instance] DirLimSpread.isAffineHom_specDiag_map
attribute [local instance] DirLimSpread.isAffineHom_D_map
attribute [local instance] DirLimSpread.compactSpace_pullback_sφ
attribute [local instance] DirLimSpread.compactSpace_D_obj
attribute [local instance] DirLimSpread.quasiSeparatedSpace_pullback_sφ
attribute [local instance] DirLimSpread.quasiSeparatedSpace_D_obj
attribute [local instance] DirLimSpread.directedSystem'
attribute [local instance] DirLimSpread.nonempty'
attribute [local instance] DirLimSpread.isDirectedOrder'
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFrameDirectLimit.DirLimSpread in
Lean source · full declaration
theorem exists_isAffineOpen_isFrameOn_preimage_of_isDirectLimit
    {ι : Type u} [Preorder ι] [Nonempty ι] [IsDirected ι (· ≤ ·)]
    {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
    [DirectedSystem G fun i j h => ⇑(φ i j h)]
    {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
    (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
    (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i))) [QuasiCompact fX]
      [QuasiSeparated fX]
    (𝓛 : (Limits.pullback fX (Spec.map (CommRingCat.ofHom (g i)))).Modules) (h𝓛 :
      Scheme.Modules.IsInvertible 𝓛) :
    ∃ (j : ι) (hij : i ≤ j) (n : ℕ) (W : ULift.{u} (Fin n) → (Limits.pullback fX (Spec.map
      (CommRingCat.ofHom (φ i j hij)))).Opens),
      (∀ k, IsAffineOpen (W k)) ∧
      ∀ (c : Limits.pullback fX (Spec.map (CommRingCat.ofHom (g i))) ⟶ Limits.pullback fX (Spec.map
        (CommRingCat.ofHom (φ i j hij)))),
        c ≫ Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (φ i j hij))) = Limits.pullback.fst
          fX (Spec.map (CommRingCat.ofHom (g i))) →
        c ≫ Limits.pullback.snd fX (Spec.map (CommRingCat.ofHom (φ i j hij))) = Limits.pullback.snd
          fX (Spec.map (CommRingCat.ofHom (g i))) ≫ Spec.map (CommRingCat.ofHom (g j)) →
        (⨆ k, c ⁻¹ᵁ W k) = ⊤ ∧
        ∃ s : ∀ k, Γ(𝓛, c ⁻¹ᵁ W k), ∀ k, Scheme.Modules.IsFrameOn (s k) (c ⁻¹ᵁ W k) := by
  classical
  have : IsDirectedOrder ι := ‹IsDirected ι (· ≤ ·)›
  have hR' := isDirectLimit' φ g i hR
  have : CompactSpace ↥X := QuasiCompact.compactSpace_of_compactSpace fX
  have : QuasiSeparatedSpace ↥X := quasiSeparatedSpace_of_quasiSeparated fX
  have hc := isLimitCone (φ' φ i) (g' g i) (bot i) (bot_le i) fX hR'
  let XR : Scheme.{u} := Limits.pullback fX (Spec.map (CommRingCat.ofHom (g i)))
  let Jt : Type u := {A : XR.Opens // IsAffineOpen A ∧ ∃ s : Γ(𝓛, A), Scheme.Modules.IsFrameOn s A}
  have hcov : IsOpenCover (fun A : Jt => (A.1 : XR.Opens)) := by
    refine IsOpenCover.mk (top_le_iff.mp fun x _ => ?_)
    obtain ⟨U, s, hxU, hs⟩ := h𝓛.exists_isFrameOn x
    obtain ⟨_, ⟨A, hA, rfl⟩, hxA, hAU⟩ := XR.isBasis_affineOpens.exists_subset_of_mem_open hxU
      U.isOpen
    have hsA : Scheme.Modules.IsFrameOn (𝓛.presheaf.map (homOfLE hAU).op s) A := (hs.map (homOfLE
      hAU)).mono hAU
    exact Opens.mem_iSup.mpr ⟨⟨A, hA, _, hsA⟩, hxA⟩
  obtain ⟨jo, S, V, hV, hVU⟩ :=
    Scheme.exists_isOpenCover_and_isAffine (D (φ' φ i) (bot i) (bot_le i) fX)
      (DirLimSpread.c (φ' φ i) (g' g i) (bot i) (bot_le i) fX hR'.compatibility) hc
      (fun A : Jt => (A.1 : XR.Opens)) hcov (fun A => A.2.1)
  obtain ⟨j⟩ := jo
  let e : ULift.{u} (Fin S.card) → ↥S := fun k => S.equivFin.symm k.down
  have he : Function.Surjective e := fun A => ⟨ULift.up (S.equivFin A), by simp [e]⟩
  refine ⟨j.1, j.2, S.card, fun k => V (e k), fun k => (hVU (e k)).1, fun cX hX₁ hX₂ => ?_⟩
  have ecX : cX = proj (φ' φ i) (g' g i) (bot_le i) fX hR'.compatibility j := by
    apply pullback.hom_ext
    · rw [hX₁]
      exact (proj_fstL (φ := φ' φ i) (g := g' g i) (hb := bot_le i) (fX := fX) (hRc :=
        hR'.compatibility) j).symm
    · rw [hX₂]
      exact (proj_sndL (φ := φ' φ i) (g := g' g i) (hb := bot_le i) (fX := fX) (hRc :=
        hR'.compatibility) j).symm
  have hpre : ∀ k, cX ⁻¹ᵁ V (e k) = (e k).1.1 := fun k => by
    rw [ecX]
    exact ((hVU (e k)).2).symm
  refine ⟨?_, ?_⟩
  · refine top_le_iff.mp fun x _ => ?_
    have hx : cX.base x ∈ (⨆ A : ↥S, V A) := by
      rw [hV.iSup_eq_top]
      exact trivial
    obtain ⟨A, hA⟩ := Opens.mem_iSup.mp hx
    obtain ⟨k, rfl⟩ := he A
    exact Opens.mem_iSup.mpr ⟨k, show x ∈ cX ⁻¹ᵁ V (e k) from hA⟩
  · have hex : ∀ k, ∃ s : Γ(𝓛, cX ⁻¹ᵁ V (e k)), Scheme.Modules.IsFrameOn s (cX ⁻¹ᵁ V (e k)) := fun
      k =>
      InvertibleFrameDirectLimit.AlgebraicGeometry.Scheme.Modules.exists_isFrameOn_congr
        (hpre k).symm (e k).1.2.2
    exact ⟨fun k => (hex k).choose, fun k => (hex k).choose_spec⟩

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