Module

exists_isPullback_glue_of_isPullback_of_isOpenImmersion.lean

Nyll.AlgebraicCurves.Geometry.Schemes.exists_isPullback_glue_of_isPullback_of_isOpenImmersion

38 declarations indexed from sourceView source ↗

Module documentation

exists is Pullback glue of is Pullback of is Open Immersion

Imports9

Mathlib.AlgebraicGeometry.PullbackCarrier
Lean.Elab.Command
Mathlib.AlgebraicGeometry.Gluing
Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Imported by2

def

F

L43 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.F

Documentation

The span of the two open pieces and their common overlap.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)

Lean source · statement

def F : WidePushoutShape Bool ⥤ Scheme.{u}

instance

F_map_isOpenImmersion

L49 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.F_map_isOpenImmersion

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)

Lean source · statement

instance F_map_isOpenImmersion : ∀ {i j : WidePushoutShape Bool} (f : i ⟶ j),
    IsOpenImmersion ((F ia ib).map f)

def

X₀

L59 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.X₀

Documentation

The scheme obtained by gluing the two open pieces.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)

Lean source · statement

def X₀ : Scheme.{u}

def

iU

L62 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.iU

Documentation

The inclusion of the first piece in the glued scheme.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)

Lean source · statement

def iU : U₀ ⟶ X₀ ia ib

def

iV

L64 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.iV

Documentation

The inclusion of the second piece in the glued scheme.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)

Lean source · statement

def iV : V₀ ⟶ X₀ ia ib

def

i0

L66 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.i0

Documentation

The common inclusion of the overlap in the glued scheme.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)

Lean source · statement

def i0 : W₀ ⟶ X₀ ia ib

instance

(anonymous instance)

L68 ↗

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)

Lean source · statement

instance : IsOpenImmersion (iU ia ib)

instance

(anonymous instance)

L70 ↗

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)

Lean source · statement

instance : IsOpenImmersion (iV ia ib)

theorem

ia_iU

L73 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.ia_iU

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)

Lean source · statement

theorem ia_iU : ia ≫ iU ia ib = i0 ia ib

theorem

ib_iV

L74 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.ib_iV

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)

Lean source · statement

theorem ib_iV : ib ≫ iV ia ib = i0 ia ib

theorem

ia_iU_eq_ib_iV

L75 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.ia_iU_eq_ib_iV

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)

Lean source · statement

theorem ia_iU_eq_ib_iV : ia ≫ iU ia ib = ib ≫ iV ia ib

def

f₀

L78 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.f₀

Documentation

The structure morphism descended from the two compatible local morphisms.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)

Lean source · statement

def f₀ : X₀ ia ib ⟶ Spec (CommRingCat.of R)

theorem

iU_f₀

L89 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.iU_f₀

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)

Lean source · statement

theorem iU_f₀ : iU ia ib ≫ f₀ u₀ v₀ ia ib hab = u₀

theorem

iV_f₀

L90 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.iV_f₀

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)

Lean source · statement

theorem iV_f₀ : iV ia ib ≫ f₀ u₀ v₀ ia ib hab = v₀

theorem

cover

L92 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.cover

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)

Lean source · statement

theorem cover (x : ↥(X₀ ia ib)) :
    x ∈ Set.range (iU ia ib).base ∨ x ∈ Set.range (iV ia ib).base

theorem

range_union

L105 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.range_union

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)

Lean source · statement

theorem range_union : Set.range (iU ia ib).base ∪ Set.range (iV ia ib).base = Set.univ

theorem

preimage_iV_iU

L108 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.preimage_iV_iU

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)

Lean source · statement

theorem preimage_iV_iU : iV ia ib ⁻¹ᵁ (iU ia ib).opensRange = ib.opensRange

theorem

isPullback_charts

L126 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.isPullback_charts

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)

Lean source · statement

theorem isPullback_charts : IsPullback ia ib (iU ia ib) (iV ia ib)

theorem

lfp

L136 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.lfp

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)
section props
variable [QuasiCompact u₀] [QuasiSeparated u₀] [LocallyOfFinitePresentation u₀]
  [QuasiCompact v₀] [QuasiSeparated v₀] [LocallyOfFinitePresentation v₀] [QuasiCompact (ia ≫ u₀)]
omit [QuasiCompact u₀] [QuasiSeparated u₀] [QuasiCompact v₀] [QuasiSeparated v₀]
  [QuasiCompact (ia ≫ u₀)] in

Lean source · statement

theorem lfp : LocallyOfFinitePresentation (f₀ u₀ v₀ ia ib hab)

theorem

qc

L154 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.qc

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)
section props
variable [QuasiCompact u₀] [QuasiSeparated u₀] [LocallyOfFinitePresentation u₀]
  [QuasiCompact v₀] [QuasiSeparated v₀] [LocallyOfFinitePresentation v₀] [QuasiCompact (ia ≫ u₀)]
omit [QuasiSeparated u₀] [LocallyOfFinitePresentation u₀] [QuasiSeparated v₀]
  [LocallyOfFinitePresentation v₀] [QuasiCompact (ia ≫ u₀)] in

Lean source · statement

theorem qc : QuasiCompact (f₀ u₀ v₀ ia ib hab)

abbrev

δ

L171 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.QSGlue.δ

Documentation

The map from the overlap to the overlap over the base.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)
namespace QSGlue
variable {S Y' : Scheme.{u}} (f' : Y' ⟶ S)

Lean source · statement

abbrev δ {P Q : Scheme.{u}} (jP : P ⟶ Y') (jQ : Q ⟶ Y') :
    pullback jP jQ ⟶ pullback (jP ≫ f') (jQ ≫ f')

theorem

quasiCompact_δ_self

L176 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.QSGlue.quasiCompact_δ_self

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)
namespace QSGlue
variable {S Y' : Scheme.{u}} (f' : Y' ⟶ S)

Lean source · statement

theorem quasiCompact_δ_self {P : Scheme.{u}} (j : P ⟶ Y') [Mono j] [QuasiSeparated (j ≫ f')] :
    QuasiCompact (δ f' j j)

theorem

quasiCompact_δ_of_isPullback

L188 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.QSGlue.quasiCompact_δ_of_isPullback

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)
namespace QSGlue
variable {S Y' : Scheme.{u}} (f' : Y' ⟶ S)

Lean source · full declaration

theorem quasiCompact_δ_of_isPullback {P Q U : Scheme.{u}} (jA : P ⟶ Y') (jB : Q ⟶ Y')
    (uA : U ⟶ P) (uB : U ⟶ Q) (hsq : IsPullback uA uB jA jB)
    (hΓ : QuasiCompact (pullback.lift uA uB
      (by rw [← Category.assoc, hsq.w, Category.assoc]) : U ⟶ pullback (jA ≫ f') (jB ≫ f'))) :
    QuasiCompact (δ f' jA jB) := by
  have h1 : hsq.isoPullback.hom ≫ δ f' jA jB =
      pullback.lift uA uB (by rw [← Category.assoc, hsq.w, Category.assoc]) := by
    apply pullback.hom_ext
    · simp only [δ, Category.assoc, pullback.lift_fst, Category.comp_id,
        IsPullback.isoPullback_hom_fst]
    · simp only [δ, Category.assoc, pullback.lift_snd, Category.comp_id,
        IsPullback.isoPullback_hom_snd]
  have h2 : δ f' jA jB = hsq.isoPullback.inv ≫
      pullback.lift uA uB (by rw [← Category.assoc, hsq.w, Category.assoc]) := by
    rw [← h1, Iso.inv_hom_id_assoc]
  rw [h2]; infer_instance

theorem

quasiCompact_δ_symm

L205 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.QSGlue.quasiCompact_δ_symm

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)
namespace QSGlue
variable {S Y' : Scheme.{u}} (f' : Y' ⟶ S)

Lean source · statement

theorem quasiCompact_δ_symm {P Q : Scheme.{u}} (jA : P ⟶ Y') (jB : Q ⟶ Y')
    [QuasiCompact (δ f' jA jB)] : QuasiCompact (δ f' jB jA)

theorem

quasiSeparated_glue

L216 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.QSGlue.quasiSeparated_glue

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)
namespace QSGlue
variable {S Y' : Scheme.{u}} (f' : Y' ⟶ S)

Lean source · full declaration

theorem quasiSeparated_glue {P Q U : Scheme.{u}}
    (jA : P ⟶ Y') (jB : Q ⟶ Y') [IsOpenImmersion jA] [IsOpenImmersion jB]
    (hcov : Set.range jA.base ∪ Set.range jB.base = Set.univ)
    [QuasiSeparated (jA ≫ f')] [QuasiSeparated (jB ≫ f')]
    (uA : U ⟶ P) (uB : U ⟶ Q) (hsq : IsPullback uA uB jA jB)
    (hΓ : QuasiCompact (pullback.lift uA uB
      (by rw [← Category.assoc, hsq.w, Category.assoc]) : U ⟶ pullback (jA ≫ f') (jB ≫ f'))) :
    QuasiSeparated f' := by
  classical
  let XU : Bool → Scheme.{u} := fun t => cond t P Q
  let fU : ∀ t : Bool, XU t ⟶ Y' := fun t => match t with
    | true => jA
    | false => jB
  have hfU : ∀ t : Bool, IsOpenImmersion (fU t) := by
    intro t; cases t
    · change IsOpenImmersion jB; infer_instance
    · change IsOpenImmersion jA; infer_instance
  let 𝒰 : Y'.OpenCover := ⟨⟨Bool, XU, fU⟩, ⟨by
      simpa using show ∀ y : Y', ∃ (t : Bool) (x : XU t), (fU t).base x = y from fun y => by
        have hy : y ∈ Set.range jA.base ∪ Set.range jB.base := by rw [hcov]; trivial
        rcases hy with ⟨x, hx⟩ | ⟨x, hx⟩
        · exact ⟨true, x, hx⟩
        · exact ⟨false, x, hx⟩, by simpa using hfU⟩⟩
  have hδ : ∀ s t : Bool, QuasiCompact (δ f' (𝒰.f s) (𝒰.f t)) := by
    intro s t
    cases s <;> cases t
    · change QuasiCompact (δ f' jB jB); exact quasiCompact_δ_self f' jB
    · change QuasiCompact (δ f' jB jA)
      have := quasiCompact_δ_of_isPullback f' jA jB uA uB hsq hΓ
      exact quasiCompact_δ_symm f' jA jB
    · change QuasiCompact (δ f' jA jB); exact quasiCompact_δ_of_isPullback f' jA jB uA uB hsq hΓ
    · change QuasiCompact (δ f' jA jA); exact quasiCompact_δ_self f' jA
  constructor
  have hAffine : HasAffineProperty @QuasiCompact (fun X _ _ _ ↦ CompactSpace X) :=
    AlgebraicGeometry.instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat
  have : MorphismProperty.RespectsIso @QuasiCompact :=
    @HasAffineProperty.instRespectsIsoScheme _ _ hAffine
  have : IsZariskiLocalAtTarget @QuasiCompact :=
    @HasAffineProperty.instIsZariskiLocalAtTarget _ _ hAffine
  apply IsZariskiLocalAtTarget.of_openCover (P := @QuasiCompact)
    (Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f' f')
  rintro ⟨s, t⟩
  have hP := pullback_map_diagonal_isPullback (𝒰.f s) (𝒰.f t) f'
  have e : hP.isoPullback.hom ≫ pullback.snd _ _ = δ f' (𝒰.f s) (𝒰.f t) := hP.isoPullback_hom_snd
  have h3 : QuasiCompact (hP.isoPullback.hom ≫ pullback.snd _ _) := by rw [e]; exact hδ s t
  exact (MorphismProperty.cancel_left_of_respectsIso @QuasiCompact hP.isoPullback.hom _).mp h3

theorem

qs

L271 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.qs

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)
section props2
variable [QuasiCompact u₀] [QuasiSeparated u₀] [LocallyOfFinitePresentation u₀]
  [QuasiCompact v₀] [QuasiSeparated v₀] [LocallyOfFinitePresentation v₀] [QuasiCompact (ia ≫ u₀)]
omit [QuasiCompact u₀] [LocallyOfFinitePresentation u₀]
  [QuasiCompact v₀] [LocallyOfFinitePresentation v₀] in

Lean source · statement

theorem qs : QuasiSeparated (f₀ u₀ v₀ ia ib hab)

def

coverX

L299 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.coverX

Documentation

The two-piece open cover of the original scheme.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)
section compare
variable {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of A))
  {U V W : Scheme.{u}} (jU : U ⟶ X) (jV : V ⟶ X) [IsOpenImmersion jU] [IsOpenImmersion jV]
  (hcov : Set.range jU.base ∪ Set.range jV.base = Set.univ)
  (kU : W ⟶ U) (kV : W ⟶ V) (hW : IsPullback kU kV jU jV)
  (πU : U ⟶ U₀) (πV : V ⟶ V₀) (πW : W ⟶ W₀) (hWU : IsPullback kU πW πU ia) (hWV : IsPullback kV πW
    πV ib)

Lean source · statement

def coverX : X.OpenCover

theorem

kU_kV_compat

L315 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.kU_kV_compat

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)
section compare
variable {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of A))
  {U V W : Scheme.{u}} (jU : U ⟶ X) (jV : V ⟶ X) [IsOpenImmersion jU] [IsOpenImmersion jV]
  (hcov : Set.range jU.base ∪ Set.range jV.base = Set.univ)
  (kU : W ⟶ U) (kV : W ⟶ V) (hW : IsPullback kU kV jU jV)
  (πU : U ⟶ U₀) (πV : V ⟶ V₀) (πW : W ⟶ W₀) (hWU : IsPullback kU πW πU ia) (hWV : IsPullback kV πW
    πV ib)
include hWU hWV in

Lean source · statement

theorem kU_kV_compat : kU ≫ πU ≫ iU ia ib = kV ≫ πV ≫ iV ia ib

def

π

L320 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.π

Documentation

The morphism obtained by gluing the two local comparison maps.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)
section compare
variable {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of A))
  {U V W : Scheme.{u}} (jU : U ⟶ X) (jV : V ⟶ X) [IsOpenImmersion jU] [IsOpenImmersion jV]
  (hcov : Set.range jU.base ∪ Set.range jV.base = Set.univ)
  (kU : W ⟶ U) (kV : W ⟶ V) (hW : IsPullback kU kV jU jV)
  (πU : U ⟶ U₀) (πV : V ⟶ V₀) (πW : W ⟶ W₀) (hWU : IsPullback kU πW πU ia) (hWV : IsPullback kV πW
    πV ib)

Lean source · statement

def π : X ⟶ X₀ ia ib

theorem

jU_π

L342 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.jU_π

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)
section compare
variable {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of A))
  {U V W : Scheme.{u}} (jU : U ⟶ X) (jV : V ⟶ X) [IsOpenImmersion jU] [IsOpenImmersion jV]
  (hcov : Set.range jU.base ∪ Set.range jV.base = Set.univ)
  (kU : W ⟶ U) (kV : W ⟶ V) (hW : IsPullback kU kV jU jV)
  (πU : U ⟶ U₀) (πV : V ⟶ V₀) (πW : W ⟶ W₀) (hWU : IsPullback kU πW πU ia) (hWV : IsPullback kV πW
    πV ib)

Lean source · statement

theorem jU_π : jU ≫ π ia ib jU jV hcov kU kV hW πU πV πW hWU hWV = πU ≫ iU ia ib

theorem

jV_π

L345 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.jV_π

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)
section compare
variable {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of A))
  {U V W : Scheme.{u}} (jU : U ⟶ X) (jV : V ⟶ X) [IsOpenImmersion jU] [IsOpenImmersion jV]
  (hcov : Set.range jU.base ∪ Set.range jV.base = Set.univ)
  (kU : W ⟶ U) (kV : W ⟶ V) (hW : IsPullback kU kV jU jV)
  (πU : U ⟶ U₀) (πV : V ⟶ V₀) (πW : W ⟶ W₀) (hWU : IsPullback kU πW πU ia) (hWV : IsPullback kV πW
    πV ib)

Lean source · statement

theorem jV_π : jV ≫ π ia ib jU jV hcov kU kV hW πU πV πW hWU hWV = πV ≫ iV ia ib

theorem

π_f₀

L355 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.π_f₀

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)
section compare
variable {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of A))
  {U V W : Scheme.{u}} (jU : U ⟶ X) (jV : V ⟶ X) [IsOpenImmersion jU] [IsOpenImmersion jV]
  (hcov : Set.range jU.base ∪ Set.range jV.base = Set.univ)
  (kU : W ⟶ U) (kV : W ⟶ V) (hW : IsPullback kU kV jU jV)
  (πU : U ⟶ U₀) (πV : V ⟶ V₀) (πW : W ⟶ W₀) (hWU : IsPullback kU πW πU ia) (hWV : IsPullback kV πW
    πV ib)
variable (hU : IsPullback πU (jU ≫ g) u₀ (Spec.map (CommRingCat.ofHom (algebraMap R A))))
  (hV : IsPullback πV (jV ≫ g) v₀ (Spec.map (CommRingCat.ofHom (algebraMap R A))))
local notation "ιR" => Spec.map (CommRingCat.ofHom (algebraMap R A))
local notation "PI" => π ia ib jU jV hcov kU kV hW πU πV πW hWU hWV
include hU hV in

Lean source · statement

theorem π_f₀ : PI ≫ f₀ u₀ v₀ ia ib hab = g ≫ ιR

theorem

preimage_π_iU

L365 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.preimage_π_iU

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)
section compare
variable {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of A))
  {U V W : Scheme.{u}} (jU : U ⟶ X) (jV : V ⟶ X) [IsOpenImmersion jU] [IsOpenImmersion jV]
  (hcov : Set.range jU.base ∪ Set.range jV.base = Set.univ)
  (kU : W ⟶ U) (kV : W ⟶ V) (hW : IsPullback kU kV jU jV)
  (πU : U ⟶ U₀) (πV : V ⟶ V₀) (πW : W ⟶ W₀) (hWU : IsPullback kU πW πU ia) (hWV : IsPullback kV πW
    πV ib)
variable (hU : IsPullback πU (jU ≫ g) u₀ (Spec.map (CommRingCat.ofHom (algebraMap R A))))
  (hV : IsPullback πV (jV ≫ g) v₀ (Spec.map (CommRingCat.ofHom (algebraMap R A))))
local notation "ιR" => Spec.map (CommRingCat.ofHom (algebraMap R A))
local notation "PI" => π ia ib jU jV hcov kU kV hW πU πV πW hWU hWV
omit hU hV

Lean source · statement

theorem preimage_π_iU : PI ⁻¹ᵁ (iU ia ib).opensRange = jU.opensRange

theorem

preimage_π_iV

L398 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.preimage_π_iV

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)
section compare
variable {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of A))
  {U V W : Scheme.{u}} (jU : U ⟶ X) (jV : V ⟶ X) [IsOpenImmersion jU] [IsOpenImmersion jV]
  (hcov : Set.range jU.base ∪ Set.range jV.base = Set.univ)
  (kU : W ⟶ U) (kV : W ⟶ V) (hW : IsPullback kU kV jU jV)
  (πU : U ⟶ U₀) (πV : V ⟶ V₀) (πW : W ⟶ W₀) (hWU : IsPullback kU πW πU ia) (hWV : IsPullback kV πW
    πV ib)
variable (hU : IsPullback πU (jU ≫ g) u₀ (Spec.map (CommRingCat.ofHom (algebraMap R A))))
  (hV : IsPullback πV (jV ≫ g) v₀ (Spec.map (CommRingCat.ofHom (algebraMap R A))))
local notation "ιR" => Spec.map (CommRingCat.ofHom (algebraMap R A))
local notation "PI" => π ia ib jU jV hcov kU kV hW πU πV πW hWU hWV
omit hU hV

Lean source · statement

theorem preimage_π_iV : PI ⁻¹ᵁ (iV ia ib).opensRange = jV.opensRange

theorem

sqU

L439 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.sqU

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)
section compare
variable {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of A))
  {U V W : Scheme.{u}} (jU : U ⟶ X) (jV : V ⟶ X) [IsOpenImmersion jU] [IsOpenImmersion jV]
  (hcov : Set.range jU.base ∪ Set.range jV.base = Set.univ)
  (kU : W ⟶ U) (kV : W ⟶ V) (hW : IsPullback kU kV jU jV)
  (πU : U ⟶ U₀) (πV : V ⟶ V₀) (πW : W ⟶ W₀) (hWU : IsPullback kU πW πU ia) (hWV : IsPullback kV πW
    πV ib)
variable (hU : IsPullback πU (jU ≫ g) u₀ (Spec.map (CommRingCat.ofHom (algebraMap R A))))
  (hV : IsPullback πV (jV ≫ g) v₀ (Spec.map (CommRingCat.ofHom (algebraMap R A))))
local notation "ιR" => Spec.map (CommRingCat.ofHom (algebraMap R A))
local notation "PI" => π ia ib jU jV hcov kU kV hW πU πV πW hWU hWV
omit hU hV

Lean source · statement

theorem sqU : IsPullback πU jU (iU ia ib) PI

theorem

sqV

L443 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.sqV

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)
section compare
variable {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of A))
  {U V W : Scheme.{u}} (jU : U ⟶ X) (jV : V ⟶ X) [IsOpenImmersion jU] [IsOpenImmersion jV]
  (hcov : Set.range jU.base ∪ Set.range jV.base = Set.univ)
  (kU : W ⟶ U) (kV : W ⟶ V) (hW : IsPullback kU kV jU jV)
  (πU : U ⟶ U₀) (πV : V ⟶ V₀) (πW : W ⟶ W₀) (hWU : IsPullback kU πW πU ia) (hWV : IsPullback kV πW
    πV ib)
variable (hU : IsPullback πU (jU ≫ g) u₀ (Spec.map (CommRingCat.ofHom (algebraMap R A))))
  (hV : IsPullback πV (jV ≫ g) v₀ (Spec.map (CommRingCat.ofHom (algebraMap R A))))
local notation "ιR" => Spec.map (CommRingCat.ofHom (algebraMap R A))
local notation "PI" => π ia ib jU jV hcov kU kV hW πU πV πW hWU hWV
omit hU hV

Lean source · statement

theorem sqV : IsPullback πV jV (iV ia ib) PI

def

coverX₀

L448 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isPullback_glue_of_isPullback_of_isOpenImmersion.TwoOpenGlue.coverX₀

Documentation

The two-piece open cover of the glued model.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace TwoOpenGlue
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
  {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
  (ia : W₀ ⟶ U₀) (ib : W₀ ⟶ V₀) [IsOpenImmersion ia] [IsOpenImmersion ib] (hab : ia ≫ u₀ = ib ≫ v₀)
section compare
variable {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of A))
  {U V W : Scheme.{u}} (jU : U ⟶ X) (jV : V ⟶ X) [IsOpenImmersion jU] [IsOpenImmersion jV]
  (hcov : Set.range jU.base ∪ Set.range jV.base = Set.univ)
  (kU : W ⟶ U) (kV : W ⟶ V) (hW : IsPullback kU kV jU jV)
  (πU : U ⟶ U₀) (πV : V ⟶ V₀) (πW : W ⟶ W₀) (hWU : IsPullback kU πW πU ia) (hWV : IsPullback kV πW
    πV ib)
variable (hU : IsPullback πU (jU ≫ g) u₀ (Spec.map (CommRingCat.ofHom (algebraMap R A))))
  (hV : IsPullback πV (jV ≫ g) v₀ (Spec.map (CommRingCat.ofHom (algebraMap R A))))
local notation "ιR" => Spec.map (CommRingCat.ofHom (algebraMap R A))
local notation "PI" => π ia ib jU jV hcov kU kV hW πU πV πW hWU hWV
omit hU hV

Lean source · statement

def coverX₀ : (X₀ ia ib).OpenCover

theorem

exists_isPullback_glue_of_isPullback_of_isOpenImmersion

L484 ↗

AlgebraicGeometry.exists_isPullback_glue_of_isPullback_of_isOpenImmersion

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_isPullback_glue_of_isPullback_of_isOpenImmersion
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
open TwoOpenGlue in

Lean source · statement

theorem _root_.AlgebraicGeometry.exists_isPullback_glue_of_isPullback_of_isOpenImmersion
    {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    {U₀ V₀ W₀ : Scheme.{u}} (u₀ : U₀ ⟶ Spec (CommRingCat.of R)) (v₀ : V₀ ⟶ Spec (CommRingCat.of R))
    (a : W₀ ⟶ U₀) (b : W₀ ⟶ V₀) [IsOpenImmersion a] [IsOpenImmersion b] (hab : a ≫ u₀ = b ≫ v₀)
    [QuasiCompact u₀] [QuasiSeparated u₀] [LocallyOfFinitePresentation u₀]
    [QuasiCompact v₀] [QuasiSeparated v₀] [LocallyOfFinitePresentation v₀] [QuasiCompact (a ≫ u₀)]
    {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of A))
    {U V W : Scheme.{u}} (jU : U ⟶ X) (jV : V ⟶ X) [IsOpenImmersion jU] [IsOpenImmersion jV]
    (hcov : Set.range jU.base ∪ Set.range jV.base = Set.univ)
    (kU : W ⟶ U) (kV : W ⟶ V) (hW : IsPullback kU kV jU jV)
    (πU : U ⟶ U₀) (hU : IsPullback πU (jU ≫ g) u₀ (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    (πV : V ⟶ V₀) (hV : IsPullback πV (jV ≫ g) v₀ (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    (πW : W ⟶ W₀) (hWU : IsPullback kU πW πU a) (hWV : IsPullback kV πW πV b) :
    ∃ (X₀ : Scheme.{u}) (f₀ : X₀ ⟶ Spec (CommRingCat.of R)) (π : X ⟶ X₀) (iU : U₀ ⟶ X₀) (iV : V₀ ⟶
      X₀),
      IsOpenImmersion iU ∧ IsOpenImmersion iV ∧ iU ≫ f₀ = u₀ ∧ iV ≫ f₀ = v₀ ∧ a ≫ iU = b ≫ iV ∧
      Set.range iU.base ∪ Set.range iV.base = Set.univ ∧ IsPullback a b iU iV ∧
      πU ≫ iU = jU ≫ π ∧ πV ≫ iV = jV ≫ π ∧
      QuasiCompact f₀ ∧ QuasiSeparated f₀ ∧ LocallyOfFinitePresentation f₀ ∧
      IsPullback π g f₀ (Spec.map (CommRingCat.ofHom (algebraMap R A)))

Module documentation

exists is Pullback glue of is Pullback of is Open Immersion

Declarations