Module

Scheme_exists_quotient_of_forall_exists_quotient_restrict.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_quotient_of_forall_exists_quotient_restrict

107 declarations indexed from sourceView source ↗

Module documentation

Scheme exists quotient of forall exists quotient restrict

Imports1

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_quotient_baseChange_of_finiteLocallyFree_of_isPullback

Imported by2

structure

MkCore

L42 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore

Documentation

Open-chart gluing data expressed with open subsets and their transition maps.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry

Lean source · full declaration

structure MkCore where
  /-- The index type of the charts. -/
  {J : Type u}
  /-- The scheme at each chart index. -/
  U : J → Scheme.{u}
  /-- The overlap open subset of each chart with another chart. -/
  V : ∀ i, J → (U i).Opens
  /-- The transition morphism from one overlap to the opposite overlap. -/
  t : ∀ i j, (V i j : Scheme.{u}) ⟶ (V j i : Scheme.{u})
  /-- A chart overlaps with itself on its whole space. -/
  V_id : ∀ i, V i i = ⊤
  /-- The self-transition is the identity morphism. -/
  t_id : ∀ i, t i i = 𝟙 _
  /-- A transition carries each triple overlap into the corresponding triple overlap. -/
  t_inter : ∀ i j k, (V i j).ι ⁻¹ᵁ (V i k) ≤ t i j ⁻¹ᵁ ((V j i).ι ⁻¹ᵁ (V j k))
  /-- The transition maps agree on triple overlaps. -/
  cocycle : ∀ i j k,
    (t i j).resLE ((V j i).ι ⁻¹ᵁ (V j k)) ((V i j).ι ⁻¹ᵁ (V i k)) (t_inter i j k) ≫
      ((U j).restrictRestrictComm (V j i) (V j k)).hom ≫ ((V j k).ι ⁻¹ᵁ (V j i)).ι ≫
        t j k ≫ (V k j).ι =
    ((U i).restrictRestrictComm (V i j) (V i k)).hom ≫ ((V i k).ι ⁻¹ᵁ (V i j)).ι ≫
      t i k ≫ (V k i).ι

abbrev

W

L70 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.W

Documentation

The triple overlap viewed as an open subset of the first pairwise overlap.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

abbrev W (i j k : h.J) : (h.V i j : Scheme.{u}).Opens

abbrev

τ

L73 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.τ

Documentation

The transition map restricted to a triple overlap.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

abbrev τ (i j k : h.J) : (h.W i j k : Scheme.{u}) ⟶ (h.W j i k : Scheme.{u})

abbrev

σ

L77 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.σ

Documentation

The canonical isomorphism exchanging the two restrictions defining a triple overlap.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

abbrev σ (i j k : h.J) : (h.W i j k : Scheme.{u}) ≅ (h.W i k j : Scheme.{u})

lemma

σ_hom_ι_ι

L80 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.σ_hom_ι_ι

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

lemma σ_hom_ι_ι (i j k : h.J) :
    (h.σ i j k).hom ≫ (h.W i k j).ι ≫ (h.V i k).ι = (h.W i j k).ι ≫ (h.V i j).ι

lemma

σ_hom_σ_hom

L84 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.σ_hom_σ_hom

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

lemma σ_hom_σ_hom (i j k : h.J) : (h.σ i j k).hom ≫ (h.σ i k j).hom = 𝟙 _

lemma

σ_self_hom_ι

L88 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.σ_self_hom_ι

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

lemma σ_self_hom_ι (i j : h.J) : (h.σ j i i).hom ≫ (h.W j i i).ι = (h.W j i i).ι

lemma

τ_ι

L91 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.τ_ι

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

lemma τ_ι (i j k : h.J) : h.τ i j k ≫ (h.W j i k).ι = (h.W i j k).ι ≫ h.t i j

lemma

cocycle'

L94 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.cocycle'

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

lemma cocycle' (i j k : h.J) :
    h.τ i j k ≫ (h.σ j i k).hom ≫ (h.W j k i).ι ≫ h.t j k ≫ (h.V k j).ι =
      (h.σ i j k).hom ≫ (h.W i k j).ι ≫ h.t i k ≫ (h.V k i).ι

lemma

W_self

L99 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.W_self

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

lemma W_self (i j : h.J) : h.W i j i = ⊤

instance

(anonymous instance)

L104 ↗

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

instance (i j : h.J) : IsIso (h.W i j i).ι

lemma

t_inv

L111 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.t_inv

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

lemma t_inv (i j : h.J) : h.t i j ≫ h.t j i = 𝟙 _

instance

(anonymous instance)

L117 ↗

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

instance (i j : h.J) : IsIso (h.t i j)

abbrev

isoW

L120 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.isoW

Documentation

Identify the pullback of two chart inclusions with their iterated open restriction.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

abbrev isoW (i j k : h.J) :
    pullback (h.V i j).ι (h.V i k).ι ≅ (h.W i j k : Scheme.{u})

def

t'

L125 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.t'

Documentation

The induced transition between the pullbacks representing triple overlaps.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

def t' (i j k : h.J) :
    pullback (h.V i j).ι (h.V i k).ι ⟶ pullback (h.V j k).ι (h.V j i).ι

lemma

core

L129 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.core

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

lemma core (i j k : h.J) :
    h.τ i j k ≫ (h.σ j i k).hom ≫ h.τ j k i ≫ (h.σ k j i).hom ≫ h.τ k i j ≫ (h.σ i k j).hom =
      𝟙 _

def

glueData

L137 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.glueData

Documentation

Convert the open-subset gluing core into the standard scheme gluing data.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · full declaration

def glueData : Scheme.GlueData.{u} where
  J := h.J
  U := h.U
  V ij := h.V ij.1 ij.2
  f i j := (h.V i j).ι
  f_id i := h.V_id i ▸ (Scheme.topIso (h.U i)).isIso_hom
  f_open i j := inferInstance
  t := h.t
  t_id := h.t_id
  t' := h.t'
  t_fac i j k := by
    change h.t' i j k ≫ pullback.snd _ _ = pullback.fst _ _ ≫ h.t i j
    rw [t', Category.assoc, Category.assoc, Category.assoc, ← pullbackRestrictIsoRestrict_hom_ι,
      Category.assoc, cancel_epi, ← cancel_mono (h.V j i).ι]
    change h.τ i j k ≫ (h.σ j i k).hom ≫ ((h.V j k).ι ∣_ h.V j i) ≫ (h.V j i).ι = _
    rw [morphismRestrict_ι, σ_hom_ι_ι, Category.assoc, τ_ι_assoc]
  cocycle i j k := by
    change h.t' i j k ≫ h.t' j k i ≫ h.t' k i j = 𝟙 _
    simp only [t', Category.assoc, Iso.inv_hom_id_assoc]
    rw [reassoc_of% (h.core i j k), Iso.hom_inv_id]

lemma

glueData_J

L158 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.glueData_J

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

lemma glueData_J : h.glueData.J = h.J

lemma

glueData_U

L159 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.glueData_U

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

lemma glueData_U (i : h.J) : h.glueData.U i = h.U i

lemma

glueData_V

L160 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.glueData_V

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

lemma glueData_V (i j : h.J) : h.glueData.V (i, j) = (h.V i j : Scheme.{u})

lemma

glueData_f

L161 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.glueData_f

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

lemma glueData_f (i j : h.J) : h.glueData.f i j = (h.V i j).ι

lemma

glueData_t

L162 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.glueData_t

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

lemma glueData_t (i j : h.J) : h.glueData.t i j = h.t i j

lemma

t_ι_ι

L164 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.t_ι_ι

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

lemma t_ι_ι (i j : h.J) :
    h.t i j ≫ (h.V j i).ι ≫ h.glueData.ι j = (h.V i j).ι ≫ h.glueData.ι i

instance

(anonymous instance)

L168 ↗

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

instance (i : h.J) : IsOpenImmersion (h.glueData.ι i)

lemma

preimage_opensRange

L171 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.GlueData.MkCore.preimage_opensRange

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme.GlueData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace MkCore
variable (h : MkCore.{u})

Lean source · statement

lemma preimage_opensRange (i j : h.J) :
    (h.glueData.ι i) ⁻¹ᵁ (h.glueData.ι j).opensRange = h.V i j

lemma

preimage_image_eq

L208 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.preimage_image_eq

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Saturation
variable {X Y R : Scheme.{u}} {s t : R ⟶ X} {p : X ⟶ Y}

Lean source · statement

lemma preimage_image_eq (hR : IsPullback s t p p) (O : X.Opens) (hO : s ⁻¹ᵁ O = t ⁻¹ᵁ O) :
    p ⁻¹' (p '' (O : Set X)) = O

lemma

isOpen_image

L218 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.isOpen_image

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Saturation
variable {X Y R : Scheme.{u}} {s t : R ⟶ X} {p : X ⟶ Y}

Lean source · statement

lemma isOpen_image [Flat p] [LocallyOfFinitePresentation p]
    (O : X.Opens) : IsOpen (p '' (O : Set X))

def

imageOpens

L223 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.imageOpens

Documentation

The open image of an open subset under a flat, locally finitely presented morphism.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Saturation
variable {X Y R : Scheme.{u}} {s t : R ⟶ X} {p : X ⟶ Y}

Lean source · statement

def imageOpens [Flat p] [LocallyOfFinitePresentation p] (O : X.Opens) : Y.Opens

lemma

coe_imageOpens

L226 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.coe_imageOpens

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Saturation
variable {X Y R : Scheme.{u}} {s t : R ⟶ X} {p : X ⟶ Y}

Lean source · statement

lemma coe_imageOpens [Flat p] [LocallyOfFinitePresentation p] (O : X.Opens) :
    (imageOpens (p := p) O : Set Y) = p '' (O : Set X)

lemma

preimage_imageOpens

L229 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.preimage_imageOpens

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Saturation
variable {X Y R : Scheme.{u}} {s t : R ⟶ X} {p : X ⟶ Y}

Lean source · statement

lemma preimage_imageOpens (hR : IsPullback s t p p) [Flat p] [LocallyOfFinitePresentation p]
    (O : X.Opens) (hO : s ⁻¹ᵁ O = t ⁻¹ᵁ O) : p ⁻¹ᵁ imageOpens (p := p) O = O

lemma

imageOpens_top

L233 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.imageOpens_top

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Saturation
variable {X Y R : Scheme.{u}} {s t : R ⟶ X} {p : X ⟶ Y}

Lean source · statement

lemma imageOpens_top [Flat p] [LocallyOfFinitePresentation p] [Surjective p] :
    imageOpens (p := p) ⊤ = ⊤

lemma

le_imageOpens_iff

L237 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.le_imageOpens_iff

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Saturation
variable {X Y R : Scheme.{u}} {s t : R ⟶ X} {p : X ⟶ Y}

Lean source · statement

lemma le_imageOpens_iff [Flat p] [LocallyOfFinitePresentation p] (O : X.Opens) (x : X) (hx : x ∈ O)
  :
    p x ∈ imageOpens (p := p) O

lemma

preimage_preimage_eq

L248 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.preimage_preimage_eq

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section RestrictPkg
variable {X Y R : Scheme.{u}} {s t : R ⟶ X} {p : X ⟶ Y}

Lean source · statement

lemma preimage_preimage_eq (hw : s ≫ p = t ≫ p) (U : Y.Opens) :
    s ⁻¹ᵁ (p ⁻¹ᵁ U) = t ⁻¹ᵁ (p ⁻¹ᵁ U)

def

tRes

L254 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.tRes

Documentation

The second relation map restricted over an open subset of the quotient.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section RestrictPkg
variable {X Y R : Scheme.{u}} {s t : R ⟶ X} {p : X ⟶ Y}

Lean source · statement

def tRes (hw : s ≫ p = t ≫ p) (U : Y.Opens) :
    (s ⁻¹ᵁ (p ⁻¹ᵁ U) : Scheme.{u}) ⟶ (p ⁻¹ᵁ U : Scheme.{u})

lemma

tRes_ι

L258 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.tRes_ι

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section RestrictPkg
variable {X Y R : Scheme.{u}} {s t : R ⟶ X} {p : X ⟶ Y}

Lean source · statement

lemma tRes_ι (hw : s ≫ p = t ≫ p) (U : Y.Opens) :
    tRes hw U ≫ (p ⁻¹ᵁ U).ι = (s ⁻¹ᵁ (p ⁻¹ᵁ U)).ι ≫ t

lemma

sRes_w

L262 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.sRes_w

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section RestrictPkg
variable {X Y R : Scheme.{u}} {s t : R ⟶ X} {p : X ⟶ Y}

Lean source · statement

lemma sRes_w (hw : s ≫ p = t ≫ p) (U : Y.Opens) :
    (s ∣_ (p ⁻¹ᵁ U)) ≫ (p ∣_ U) = tRes hw U ≫ (p ∣_ U)

theorem

restrict_pkg

L267 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.restrict_pkg

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section RestrictPkg
variable {X Y R : Scheme.{u}} {s t : R ⟶ X} {p : X ⟶ Y}

Lean source · statement

theorem restrict_pkg (hw : s ≫ p = t ≫ p) [IsFinite p] [Flat p] [LocallyOfFinitePresentation p]
    [Surjective p] (hR : IsPullback s t p p) (U : Y.Opens) :
    IsFinite (p ∣_ U) ∧ Flat (p ∣_ U) ∧ LocallyOfFinitePresentation (p ∣_ U) ∧
      Surjective (p ∣_ U) ∧ IsPullback (s ∣_ (p ⁻¹ᵁ U)) (tRes hw U) (p ∣_ U) (p ∣_ U) ∧
      Nonempty (IsColimit (Cofork.ofπ (p ∣_ U) (sRes_w hw U)))

def

quotIso

L285 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.quotIso

Documentation

The isomorphism between quotient schemes induced by an isomorphism of their coequalizer diagrams.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Compare
variable {R₁ X₁ Y₁ R₂ X₂ Y₂ : Scheme.{u}} {s₁ t₁ : R₁ ⟶ X₁} {s₂ t₂ : R₂ ⟶ X₂}
  {p₁ : X₁ ⟶ Y₁} {p₂ : X₂ ⟶ Y₂} {w₁ : s₁ ≫ p₁ = t₁ ≫ p₁} {w₂ : s₂ ≫ p₂ = t₂ ≫ p₂}

Lean source · statement

def quotIso (h₁ : IsColimit (Cofork.ofπ p₁ w₁)) (h₂ : IsColimit (Cofork.ofπ p₂ w₂))
    (eR : R₁ ≅ R₂) (eX : X₁ ≅ X₂) (hs : s₁ ≫ eX.hom = eR.hom ≫ s₂) (ht : t₁ ≫ eX.hom = eR.hom ≫ t₂)
      :
    Y₁ ≅ Y₂

lemma

π_quotIso_hom

L291 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.π_quotIso_hom

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Compare
variable {R₁ X₁ Y₁ R₂ X₂ Y₂ : Scheme.{u}} {s₁ t₁ : R₁ ⟶ X₁} {s₂ t₂ : R₂ ⟶ X₂}
  {p₁ : X₁ ⟶ Y₁} {p₂ : X₂ ⟶ Y₂} {w₁ : s₁ ≫ p₁ = t₁ ≫ p₁} {w₂ : s₂ ≫ p₂ = t₂ ≫ p₂}

Lean source · statement

lemma π_quotIso_hom (h₁ : IsColimit (Cofork.ofπ p₁ w₁)) (h₂ : IsColimit (Cofork.ofπ p₂ w₂))
    (eR : R₁ ≅ R₂) (eX : X₁ ≅ X₂) (hs : s₁ ≫ eX.hom = eR.hom ≫ s₂) (ht : t₁ ≫ eX.hom = eR.hom ≫ t₂)
      :
    p₁ ≫ (quotIso h₁ h₂ eR eX hs ht).hom = eX.hom ≫ p₂

abbrev

tW

L306 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.tW

Documentation

Restrict the second relation map to the invariant open neighborhood W x.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)

Lean source · statement

abbrev tW (x : X) : (s ⁻¹ᵁ W x : Scheme.{u}) ⟶ (W x : Scheme.{u})

lemma

tW_ι

L309 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.tW_ι

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)

Lean source · statement

lemma tW_ι (x : X) : tW s t W hinv x ≫ (W x).ι = (s ⁻¹ᵁ W x).ι ≫ t

def

Yloc

L318 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.Yloc

Documentation

The quotient scheme chosen for the invariant open neighborhood W x.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)

Lean source · statement

def Yloc (x : X) : Scheme.{u}

def

ploc

L321 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.ploc

Documentation

The chosen quotient morphism on the invariant open neighborhood W x.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)

Lean source · statement

def ploc (x : X) : (W x : Scheme.{u}) ⟶ Yloc s t W hinv loc x

lemma

ploc_spec

L323 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.ploc_spec

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)

Lean source · statement

lemma ploc_spec (x : X) :
    (s ∣_ W x) ≫ ploc s t W hinv loc x = tW s t W hinv x ≫ ploc s t W hinv loc x ∧
      IsFinite (ploc s t W hinv loc x) ∧ Flat (ploc s t W hinv loc x) ∧
      LocallyOfFinitePresentation (ploc s t W hinv loc x) ∧ Surjective (ploc s t W hinv loc x) ∧
      IsPullback (s ∣_ W x) (tW s t W hinv x) (ploc s t W hinv loc x) (ploc s t W hinv loc x)

instance

(anonymous instance)

L330 ↗

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)

Lean source · statement

instance (x : X) : IsFinite (ploc s t W hinv loc x)

instance

(anonymous instance)

L331 ↗

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)

Lean source · statement

instance (x : X) : Flat (ploc s t W hinv loc x)

instance

(anonymous instance)

L332 ↗

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)

Lean source · statement

instance (x : X) : LocallyOfFinitePresentation (ploc s t W hinv loc x)

instance

(anonymous instance)

L334 ↗

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)

Lean source · statement

instance (x : X) : Surjective (ploc s t W hinv loc x)

lemma

inv_overlap

L337 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.inv_overlap

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)

Lean source · statement

lemma inv_overlap (x y : X) :
    (s ∣_ W x) ⁻¹ᵁ ((W x).ι ⁻¹ᵁ W y) = (tW s t W hinv x) ⁻¹ᵁ ((W x).ι ⁻¹ᵁ W y)

def

V

L344 ↗

AlgebraicGeometry.Scheme.QuotGlue.V

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)

Lean source · statement

def _root_.AlgebraicGeometry.Scheme.QuotGlue.V (x y : X) : (Yloc s t W hinv
  loc x).Opens

lemma

preimage_V

L349 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.preimage_V

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue

Lean source · statement

lemma preimage_V (x y : X) : ploc s t W hinv loc x ⁻¹ᵁ V s t W hinv loc x y = (W x).ι ⁻¹ᵁ W y

lemma

range_overlap

L352 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.range_overlap

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue

Lean source · statement

lemma range_overlap (x y : X) :
    Set.range ((ploc s t W hinv loc x ⁻¹ᵁ V s t W hinv loc x y).ι ≫ (W x).ι) =
      (W x ⊓ W y : X.Opens)

lemma

hw

L363 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.hw

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue
variable {s t W hinv}

Lean source · statement

lemma hw (x : X) : (s ∣_ W x) ≫ ploc s t W hinv loc x = tW s t W hinv x ≫ ploc s t W hinv loc x

lemma

hpb

L366 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.hpb

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue
variable {s t W hinv}

Lean source · statement

lemma hpb (x : X) :
    IsPullback (s ∣_ W x) (tW s t W hinv x) (ploc s t W hinv loc x) (ploc s t W hinv loc x)

abbrev

pV

L371 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.pV

Documentation

The local quotient morphism restricted to the overlap with the neighborhood W y.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue
variable {s t W hinv}

Lean source · statement

abbrev pV (x y : X)

def

coeqV

L374 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.coeqV

Documentation

The coequalizer certificate for the local quotient restricted to an overlap.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue
variable {s t W hinv}

Lean source · statement

def coeqV (x y : X) :
    IsColimit (Cofork.ofπ (pV loc x y) (sRes_w (hw loc x) (V s t W hinv loc x y)))

lemma

isPullback_V

L378 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.isPullback_V

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue
variable {s t W hinv}

Lean source · statement

lemma isPullback_V (x y : X) :
    IsPullback ((s ∣_ W x) ∣_ (ploc s t W hinv loc x ⁻¹ᵁ V s t W hinv loc x y))
      (tRes (hw loc x) (V s t W hinv loc x y)) (pV loc x y) (pV loc x y)

def

eX

L384 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.eX

Documentation

Identify the two source restrictions representing the same overlap in X.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue
variable {s t W hinv}

Lean source · statement

def eX (x y : X) :
    (ploc s t W hinv loc x ⁻¹ᵁ V s t W hinv loc x y : Scheme.{u}) ≅
      (ploc s t W hinv loc y ⁻¹ᵁ V s t W hinv loc y x : Scheme.{u})

lemma

eX_hom_ι

L390 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.eX_hom_ι

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue
variable {s t W hinv}

Lean source · statement

lemma eX_hom_ι (x y : X) :
    (eX loc x y).hom ≫ Scheme.Opens.ι _ ≫ (W y).ι = Scheme.Opens.ι _ ≫ (W x).ι

lemma

sres_preimage

L394 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.sres_preimage

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue
variable {s t W hinv}

Lean source · statement

lemma sres_preimage (x y : X) :
    (s ∣_ W x) ⁻¹ᵁ (ploc s t W hinv loc x ⁻¹ᵁ V s t W hinv loc x y) = (s ⁻¹ᵁ W x).ι ⁻¹ᵁ (s ⁻¹ᵁ W y)

lemma

range_roverlap

L402 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.range_roverlap

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue
variable {s t W hinv}

Lean source · statement

lemma range_roverlap (x y : X) :
    Set.range (((s ∣_ W x) ⁻¹ᵁ (ploc s t W hinv loc x ⁻¹ᵁ V s t W hinv loc x y)).ι ≫ (s ⁻¹ᵁ W x).ι)
      =
      (s ⁻¹ᵁ W x ⊓ s ⁻¹ᵁ W y : R.Opens)

def

eR

L413 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.eR

Documentation

Identify the two restrictions of the relation scheme over an overlap.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue
variable {s t W hinv}

Lean source · statement

def eR (x y : X) :
    ((s ∣_ W x) ⁻¹ᵁ (ploc s t W hinv loc x ⁻¹ᵁ V s t W hinv loc x y) : Scheme.{u}) ≅
      ((s ∣_ W y) ⁻¹ᵁ (ploc s t W hinv loc y ⁻¹ᵁ V s t W hinv loc y x) : Scheme.{u})

lemma

eR_hom_ι

L419 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.eR_hom_ι

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue
variable {s t W hinv}

Lean source · statement

lemma eR_hom_ι (x y : X) :
    (eR loc x y).hom ≫ Scheme.Opens.ι _ ≫ (s ⁻¹ᵁ W y).ι = Scheme.Opens.ι _ ≫ (s ⁻¹ᵁ W x).ι

lemma

hs_comm

L423 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.hs_comm

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue
variable {s t W hinv}

Lean source · statement

lemma hs_comm (x y : X) :
    ((s ∣_ W x) ∣_ (ploc s t W hinv loc x ⁻¹ᵁ V s t W hinv loc x y)) ≫ (eX loc x y).hom =
      (eR loc x y).hom ≫ ((s ∣_ W y) ∣_ (ploc s t W hinv loc y ⁻¹ᵁ V s t W hinv loc y x))

lemma

ht_comm

L431 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.ht_comm

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue
variable {s t W hinv}

Lean source · statement

lemma ht_comm (x y : X) :
    tRes (hw loc x) (V s t W hinv loc x y) ≫ (eX loc x y).hom =
      (eR loc x y).hom ≫ tRes (hw loc y) (V s t W hinv loc y x)

def

φ

L440 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.φ

Documentation

The transition isomorphism between the two local quotient overlap schemes.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue
variable {s t W hinv}

Lean source · statement

def φ (x y : X) :
    (V s t W hinv loc x y : Scheme.{u}) ≅ (V s t W hinv loc y x : Scheme.{u})

lemma

pV_φ_hom

L445 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.pV_φ_hom

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue
variable {s t W hinv}

Lean source · statement

lemma pV_φ_hom (x y : X) : pV loc x y ≫ (φ loc x y).hom = (eX loc x y).hom ≫ pV loc y x

lemma

V_self

L448 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.V_self

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue
variable {s t W hinv}

Lean source · statement

lemma V_self (x : X) : V s t W hinv loc x x = ⊤

instance

epi_pV

L452 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.epi_pV

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue
variable {s t W hinv}

Lean source · statement

instance epi_pV (x y : X) : Epi (pV loc x y)

lemma

eX_self

L459 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.eX_self

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue
variable {s t W hinv}

Lean source · statement

lemma eX_self (x : X) : (eX loc x x).hom = 𝟙 _

lemma

φ_self

L462 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.φ_self

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X → X.Opens) (hxW : ∀ x, x ∈ W x)
  (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
variable (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue
variable {s t W hinv}

Lean source · statement

lemma φ_self (x : X) : (φ loc x x).hom = 𝟙 _

instance

isFinite_pV

L489 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.isFinite_pV

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Core
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens}
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)

Lean source · statement

instance isFinite_pV (x y : X) : IsFinite (pV loc x y)

instance

flat_pV

L491 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.flat_pV

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Core
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens}
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)

Lean source · statement

instance flat_pV (x y : X) : Flat (pV loc x y)

instance

lfp_pV

L493 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.lfp_pV

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Core
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens}
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)

Lean source · statement

instance lfp_pV (x y : X) : LocallyOfFinitePresentation (pV loc x y)

instance

surj_pV

L495 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.surj_pV

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Core
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens}
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)

Lean source · statement

instance surj_pV (x y : X) : Surjective (pV loc x y)

instance

epi_pV_restrict

L498 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.epi_pV_restrict

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Core
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens}
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)

Lean source · statement

instance epi_pV_restrict (x y : X) (O : (V s t W hinv loc x y : Scheme.{u}).Opens) :
    Epi (pV loc x y ∣_ O)

lemma

ι_mem_preimage_V

L506 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.ι_mem_preimage_V

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Core
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens}
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)

Lean source · statement

lemma ι_mem_preimage_V {x y z : X} (u : ↑(ploc s t W hinv loc x ⁻¹ᵁ V s t W hinv loc x y))
    (hu : ((ploc s t W hinv loc x ⁻¹ᵁ V s t W hinv loc x y).ι ≫ ploc s t W hinv loc x) u ∈
      V s t W hinv loc x z) :
    (ploc s t W hinv loc x ⁻¹ᵁ V s t W hinv loc x y).ι u ∈
      ploc s t W hinv loc x ⁻¹ᵁ V s t W hinv loc x z

lemma

core_t_inter

L513 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.core_t_inter

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Core
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens}
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)

Lean source · statement

lemma core_t_inter (x y z : X) :
    (V s t W hinv loc x y).ι ⁻¹ᵁ (V s t W hinv loc x z) ≤
      (φ loc x y).hom ⁻¹ᵁ ((V s t W hinv loc y x).ι ⁻¹ᵁ (V s t W hinv loc y z))

lemma

core_cocycle

L532 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.core_cocycle

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Core
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens}
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)

Lean source · statement

lemma core_cocycle (x y z : X) :
    ((φ loc x y).hom.resLE ((V s t W hinv loc y x).ι ⁻¹ᵁ (V s t W hinv loc y z))
        ((V s t W hinv loc x y).ι ⁻¹ᵁ (V s t W hinv loc x z)) (core_t_inter loc x y z) ≫
      ((Yloc s t W hinv loc y).restrictRestrictComm (V s t W hinv loc y x)
          (V s t W hinv loc y z)).hom ≫
        ((V s t W hinv loc y z).ι ⁻¹ᵁ (V s t W hinv loc y x)).ι ≫
          (φ loc y z).hom ≫ (V s t W hinv loc z y).ι) =
    ((Yloc s t W hinv loc x).restrictRestrictComm (V s t W hinv loc x y)
        (V s t W hinv loc x z)).hom ≫
      ((V s t W hinv loc x z).ι ⁻¹ᵁ (V s t W hinv loc x y)).ι ≫
        (φ loc x z).hom ≫ (V s t W hinv loc z x).ι

def

core

L647 ↗

AlgebraicGeometry.Scheme.QuotGlue.core

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Core
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens}
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)

Lean source · full declaration

def _root_.AlgebraicGeometry.Scheme.QuotGlue.core :
  Scheme.GlueData.MkCore.{u} where
  U := Yloc s t W hinv loc
  V := V s t W hinv loc
  t x y := (φ loc x y).hom
  V_id := V_self loc
  t_id := φ_self loc
  t_inter := core_t_inter loc
  cocycle := core_cocycle loc

lemma

core_J

L658 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.core_J

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Core
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens}
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue

Lean source · statement

lemma core_J : (core loc).J = X

lemma

core_U

L659 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.core_U

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Core
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens}
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue

Lean source · statement

lemma core_U (x : X) : (core loc).U x = Yloc s t W hinv loc x

lemma

core_V

L660 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.core_V

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Core
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens}
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue

Lean source · statement

lemma core_V (x y : X) : (core loc).V x y = V s t W hinv loc x y

lemma

core_t

L661 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.core_t

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Core
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens}
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
open _root_.AlgebraicGeometry.Scheme.QuotGlue

Lean source · statement

lemma core_t (x y : X) : (core loc).t x y = (φ loc x y).hom

abbrev

D

L688 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.D

Documentation

The gluing data assembled from the chosen local quotient schemes.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)

Lean source · statement

abbrev D

instance

(anonymous instance)

L690 ↗

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)

Lean source · statement

instance (x : X) : IsOpenImmersion ((D loc).ι x)

def

coverW

L694 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.coverW

Documentation

The cover of X by the chosen invariant open neighborhoods.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
local instance (x : X) : IsOpenImmersion ((D loc).ι x) :=
  Scheme.GlueData.ι_isOpenImmersion (D loc) (show (D loc).J from x)

Lean source · statement

def coverW : X.OpenCover

lemma

coverW_f

L698 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.coverW_f

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
local instance (x : X) : IsOpenImmersion ((D loc).ι x) :=
  Scheme.GlueData.ι_isOpenImmersion (D loc) (show (D loc).J from x)

Lean source · statement

lemma coverW_f (x : X) : (coverW hxW).f x = (W x).ι

abbrev

chart

L701 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.chart

Documentation

The local quotient morphism followed by its inclusion into the glued quotient.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
local instance (x : X) : IsOpenImmersion ((D loc).ι x) :=
  Scheme.GlueData.ι_isOpenImmersion (D loc) (show (D loc).J from x)

Lean source · statement

abbrev chart (x : X) : (W x : Scheme.{u}) ⟶ (D loc).glued

def

liftOverlap

L705 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.liftOverlap

Documentation

Lift a morphism into an overlap when its image lies in the other neighborhood.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
local instance (x : X) : IsOpenImmersion ((D loc).ι x) :=
  Scheme.GlueData.ι_isOpenImmersion (D loc) (show (D loc).J from x)

Lean source · statement

def liftOverlap {T : Scheme.{u}} (x y : X) (a : T ⟶ (W x : Scheme.{u}))
    (ha : Set.range (a ≫ (W x).ι) ⊆ (W y : Set X)) :
    T ⟶ (ploc s t W hinv loc x ⁻¹ᵁ V s t W hinv loc x y : Scheme.{u})

lemma

liftOverlap_ι

L713 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.liftOverlap_ι

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
local instance (x : X) : IsOpenImmersion ((D loc).ι x) :=
  Scheme.GlueData.ι_isOpenImmersion (D loc) (show (D loc).J from x)

Lean source · statement

lemma liftOverlap_ι {T : Scheme.{u}} (x y : X) (a : T ⟶ (W x : Scheme.{u}))
    (ha : Set.range (a ≫ (W x).ι) ⊆ (W y : Set X)) :
    liftOverlap loc x y a ha ≫ Scheme.Opens.ι _ = a

lemma

chart_comp_eq

L718 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.chart_comp_eq

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
local instance (x : X) : IsOpenImmersion ((D loc).ι x) :=
  Scheme.GlueData.ι_isOpenImmersion (D loc) (show (D loc).J from x)

Lean source · statement

lemma chart_comp_eq {T : Scheme.{u}} (x y : X) (a : T ⟶ (W x : Scheme.{u}))
    (b : T ⟶ (W y : Scheme.{u})) (hab : a ≫ (W x).ι = b ≫ (W y).ι) :
    a ≫ chart loc x = b ≫ chart loc y

def

pglued

L752 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.pglued

Documentation

The quotient morphism obtained by gluing the compatible local quotient morphisms.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
local instance (x : X) : IsOpenImmersion ((D loc).ι x) :=
  Scheme.GlueData.ι_isOpenImmersion (D loc) (show (D loc).J from x)

Lean source · statement

def pglued : X ⟶ (D loc).glued

lemma

ι_pglued

L756 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.ι_pglued

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
local instance (x : X) : IsOpenImmersion ((D loc).ι x) :=
  Scheme.GlueData.ι_isOpenImmersion (D loc) (show (D loc).J from x)

Lean source · statement

lemma ι_pglued (x : X) : (W x).ι ≫ pglued hxW loc = chart loc x

lemma

s_pglued

L759 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.s_pglued

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
local instance (x : X) : IsOpenImmersion ((D loc).ι x) :=
  Scheme.GlueData.ι_isOpenImmersion (D loc) (show (D loc).J from x)

Lean source · statement

lemma s_pglued : s ≫ pglued hxW loc = t ≫ pglued hxW loc

lemma

preimage_chart

L771 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.preimage_chart

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
local instance (x : X) : IsOpenImmersion ((D loc).ι x) :=
  Scheme.GlueData.ι_isOpenImmersion (D loc) (show (D loc).J from x)

Lean source · statement

lemma preimage_chart (x : X) :
    pglued hxW loc ⁻¹ᵁ ((D loc).ι x).opensRange = (W x).ι.opensRange

def

ιY

L799 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.ιY

Documentation

The inclusion of a chosen local quotient scheme into the glued quotient.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
local instance (x : X) : IsOpenImmersion ((D loc).ι x) :=
  Scheme.GlueData.ι_isOpenImmersion (D loc) (show (D loc).J from x)

Lean source · statement

def ιY (x : X) : Yloc s t W hinv loc x ⟶ (D loc).glued

lemma

ιY_def

L801 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.ιY_def

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
local instance (x : X) : IsOpenImmersion ((D loc).ι x) :=
  Scheme.GlueData.ι_isOpenImmersion (D loc) (show (D loc).J from x)

Lean source · statement

lemma ιY_def (x : X) : ιY loc x = (D loc).ι x

instance

isOpenImmersion_ιY

L803 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.isOpenImmersion_ιY

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
local instance (x : X) : IsOpenImmersion ((D loc).ι x) :=
  Scheme.GlueData.ι_isOpenImmersion (D loc) (show (D loc).J from x)

Lean source · statement

instance isOpenImmersion_ιY (x : X) : IsOpenImmersion (ιY loc x)

lemma

isPullback_chart

L806 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.isPullback_chart

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
local instance (x : X) : IsOpenImmersion ((D loc).ι x) :=
  Scheme.GlueData.ι_isOpenImmersion (D loc) (show (D loc).J from x)

Lean source · statement

lemma isPullback_chart (x : X) :
    IsPullback (ploc s t W hinv loc x) (W x).ι (ιY loc x) (pglued hxW loc)

lemma

isFinite_pglued

L811 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.isFinite_pglued

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
local instance (x : X) : IsOpenImmersion ((D loc).ι x) :=
  Scheme.GlueData.ι_isOpenImmersion (D loc) (show (D loc).J from x)

Lean source · statement

lemma isFinite_pglued : IsFinite (pglued hxW loc)

lemma

flat_pglued

L827 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.flat_pglued

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
local instance (x : X) : IsOpenImmersion ((D loc).ι x) :=
  Scheme.GlueData.ι_isOpenImmersion (D loc) (show (D loc).J from x)

Lean source · statement

lemma flat_pglued : Flat (pglued hxW loc)

lemma

lfp_pglued

L841 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.lfp_pglued

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
local instance (x : X) : IsOpenImmersion ((D loc).ι x) :=
  Scheme.GlueData.ι_isOpenImmersion (D loc) (show (D loc).J from x)

Lean source · statement

lemma lfp_pglued : LocallyOfFinitePresentation (pglued hxW loc)

lemma

surjective_pglued

L857 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.surjective_pglued

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
local instance (x : X) : IsOpenImmersion ((D loc).ι x) :=
  Scheme.GlueData.ι_isOpenImmersion (D loc) (show (D loc).J from x)

Lean source · statement

lemma surjective_pglued : Surjective (pglued hxW loc)

lemma

isPullback_pglued

L865 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.isPullback_pglued

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
local instance (x : X) : IsOpenImmersion ((D loc).ι x) :=
  Scheme.GlueData.ι_isOpenImmersion (D loc) (show (D loc).J from x)

Lean source · statement

lemma isPullback_pglued : IsPullback s t (pglued hxW loc) (pglued hxW loc)

theorem

main

L884 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_forall_exists_quotient_restrict.AlgebraicGeometry.Scheme.QuotGlue.main

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace QuotGlue
open _root_.AlgebraicGeometry.Scheme.QuotGlue
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main56
variable {X R : Scheme.{u}} {s t : R ⟶ X} {W : X → X.Opens} (hxW : ∀ x, x ∈ W x)
  {hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x}
  (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p)
local instance (x : X) : IsOpenImmersion ((D loc).ι x) :=
  Scheme.GlueData.ι_isOpenImmersion (D loc) (show (D loc).J from x)
include hxW loc in

Lean source · statement

theorem main :
    ∃ (Y : Scheme.{u}) (p : X ⟶ Y) (w : s ≫ p = t ≫ p),
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback s t p p ∧ Nonempty (IsColimit (Cofork.ofπ p w))

theorem

exists_quotient_of_forall_exists_quotient_restrict

L902 ↗

AlgebraicGeometry.Scheme.exists_quotient_of_forall_exists_quotient_restrict

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_forall_exists_quotient_restrict
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
universe u

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.exists_quotient_of_forall_exists_quotient_restrict
    {X R : Scheme.{u}} (s t : R ⟶ X)
    (W : X → X.Opens) (hxW : ∀ x, x ∈ W x) (hinv : ∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x)
    (loc : ∀ x, ∃ (Y : Scheme.{u}) (p : (W x).toScheme ⟶ Y),
      (s ∣_ W x) ≫ p = ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) ≫ p ∧
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (s ∣_ W x) ((R.isoOfEq (hinv x)).hom ≫ (t ∣_ W x)) p p) :
    ∃ (Y : Scheme.{u}) (p : X ⟶ Y) (w : s ≫ p = t ≫ p),
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback s t p p ∧ Nonempty (IsColimit (Cofork.ofπ p w))

Module documentation

Scheme exists quotient of forall exists quotient restrict

Declarations