NYLL
Module

Scheme_exists_quotient_of_finiteLocallyFree_equivalenceRelation.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_quotient_of_finiteLocallyFree_equivalenceRelation
18 declarations indexed from sourceView source ↗

Module documentation

Scheme exists quotient of finite Locally Free equivalence Relation

Imports3
Imported by4

Declarations

theorem

exists_invariant_affine_cover

L33 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_finiteLocallyFree_equivalenceRelation.Q1SCH.exists_invariant_affine_cover
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace Q1SCH
open _root_.AlgebraicGeometry.Scheme in
Lean source · full declaration
theorem exists_invariant_affine_cover
    {X R : Scheme.{u}} (s t : R ⟶ X)
    [IsFinite s] [Flat s] [LocallyOfFinitePresentation s]
    [IsFinite t] [Flat t] [LocallyOfFinitePresentation t]
    (hequiv : ∀ T : Scheme.{u},
      _root_.Equivalence fun x y : T ⟶ X => ∃ φ : T ⟶ R, φ ≫ s = x ∧ φ ≫ t = y)
    (haff : ∀ x : X, ∃ U : X.Opens, IsAffineOpen U ∧ ∀ r : R, s r = x → t r ∈ U) :
    ∃ W : X → X.Opens, (∀ x, IsAffineOpen (W x)) ∧ (∀ x, x ∈ W x) ∧ (∀ x, s ⁻¹ᵁ W x = t ⁻¹ᵁ W x) :=
      by
  choose U hU hxU using haff
  choose W hW hxW _ hinv using fun x =>
    exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
      s t hequiv (hU x) (hxU x)
  exact ⟨W, hW, hxW, hinv⟩
def

sW

L53 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_finiteLocallyFree_equivalenceRelation.Q1SCH.sW
Documentation

The first relation map restricted to the invariant open subset W.

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_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace Q1SCH
section restrict
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X.Opens) (hinv : s ⁻¹ᵁ W = t ⁻¹ᵁ W)
Lean source · statement
def sW : (s ⁻¹ᵁ W).toScheme ⟶ W.toScheme
def

tW

L56 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_finiteLocallyFree_equivalenceRelation.Q1SCH.tW
Documentation

The second relation map restricted to W, identified with the first preimage by hinv.

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_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace Q1SCH
section restrict
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X.Opens) (hinv : s ⁻¹ᵁ W = t ⁻¹ᵁ W)
Lean source · statement
def tW : (s ⁻¹ᵁ W).toScheme ⟶ W.toScheme
theorem

sW_ι

L58 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_finiteLocallyFree_equivalenceRelation.Q1SCH.sW_ι
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_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace Q1SCH
section restrict
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X.Opens) (hinv : s ⁻¹ᵁ W = t ⁻¹ᵁ W)
Lean source · statement
theorem sW_ι : sW s W ≫ W.ι = (s ⁻¹ᵁ W).ι ≫ s
theorem

tW_ι

L60 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_finiteLocallyFree_equivalenceRelation.Q1SCH.tW_ι
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_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace Q1SCH
section restrict
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X.Opens) (hinv : s ⁻¹ᵁ W = t ⁻¹ᵁ W)
Lean source · statement
theorem tW_ι : tW s t W hinv ≫ W.ι = (s ⁻¹ᵁ W).ι ≫ t
theorem

isPullback_sW

L62 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_finiteLocallyFree_equivalenceRelation.Q1SCH.isPullback_sW
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_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace Q1SCH
section restrict
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X.Opens) (hinv : s ⁻¹ᵁ W = t ⁻¹ᵁ W)
Lean source · statement
theorem isPullback_sW : IsPullback (s ⁻¹ᵁ W).ι (sW s W) s W.ι
theorem

isPullback_tW

L65 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_finiteLocallyFree_equivalenceRelation.Q1SCH.isPullback_tW
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_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace Q1SCH
section restrict
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X.Opens) (hinv : s ⁻¹ᵁ W = t ⁻¹ᵁ W)
Lean source · statement
theorem isPullback_tW : IsPullback (s ⁻¹ᵁ W).ι (tW s t W hinv) t W.ι
instance

(anonymous instance)

L72 ↗
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_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace Q1SCH
section restrict
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X.Opens) (hinv : s ⁻¹ᵁ W = t ⁻¹ᵁ W)
Lean source · statement
instance [IsFinite s] : IsFinite (sW s W)
instance

(anonymous instance)

L74 ↗
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_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace Q1SCH
section restrict
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X.Opens) (hinv : s ⁻¹ᵁ W = t ⁻¹ᵁ W)
Lean source · statement
instance [Flat s] : Flat (sW s W)
instance

(anonymous instance)

L76 ↗
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_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace Q1SCH
section restrict
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X.Opens) (hinv : s ⁻¹ᵁ W = t ⁻¹ᵁ W)
Lean source · statement
instance [LocallyOfFinitePresentation s] : LocallyOfFinitePresentation (sW s W)
theorem

tW_finite

L79 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_finiteLocallyFree_equivalenceRelation.Q1SCH.tW_finite
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_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace Q1SCH
section restrict
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X.Opens) (hinv : s ⁻¹ᵁ W = t ⁻¹ᵁ W)
Lean source · statement
theorem tW_finite [IsFinite t] : IsFinite (tW s t W hinv)
theorem

tW_flat

L81 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_finiteLocallyFree_equivalenceRelation.Q1SCH.tW_flat
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_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace Q1SCH
section restrict
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X.Opens) (hinv : s ⁻¹ᵁ W = t ⁻¹ᵁ W)
Lean source · statement
theorem tW_flat [Flat t] : Flat (tW s t W hinv)
theorem

tW_lfp

L83 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_finiteLocallyFree_equivalenceRelation.Q1SCH.tW_lfp
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_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace Q1SCH
section restrict
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X.Opens) (hinv : s ⁻¹ᵁ W = t ⁻¹ᵁ W)
Lean source · statement
theorem tW_lfp [LocallyOfFinitePresentation t] : LocallyOfFinitePresentation (tW s t W hinv)
theorem

mono_restrict

L87 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_finiteLocallyFree_equivalenceRelation.Q1SCH.mono_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_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace Q1SCH
section restrict
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X.Opens) (hinv : s ⁻¹ᵁ W = t ⁻¹ᵁ W)
Lean source · statement
theorem mono_restrict
    (hmono : ∀ {T : Scheme.{u}} (a b : T ⟶ R), a ≫ s = b ≫ s → a ≫ t = b ≫ t → a = b)
    {T : Scheme.{u}} (a b : T ⟶ (s ⁻¹ᵁ W).toScheme) (h₁ : a ≫ sW s W = b ≫ sW s W)
    (h₂ : a ≫ tW s t W hinv = b ≫ tW s t W hinv) : a = b
theorem

rel_restrict_iff

L96 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_finiteLocallyFree_equivalenceRelation.Q1SCH.rel_restrict_iff
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_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace Q1SCH
section restrict
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X.Opens) (hinv : s ⁻¹ᵁ W = t ⁻¹ᵁ W)
Lean source · statement
theorem rel_restrict_iff {T : Scheme.{u}} (x y : T ⟶ W.toScheme) :
    (∃ φ : T ⟶ (s ⁻¹ᵁ W).toScheme, φ ≫ sW s W = x ∧ φ ≫ tW s t W hinv = y) ↔
      ∃ ψ : T ⟶ R, ψ ≫ s = x ≫ W.ι ∧ ψ ≫ t = y ≫ W.ι
theorem

equivalence_restrict

L114 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_finiteLocallyFree_equivalenceRelation.Q1SCH.equivalence_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_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace Q1SCH
section restrict
variable {X R : Scheme.{u}} (s t : R ⟶ X) (W : X.Opens) (hinv : s ⁻¹ᵁ W = t ⁻¹ᵁ W)
Lean source · full declaration
theorem equivalence_restrict
    (hequiv : ∀ T : Scheme.{u},
      _root_.Equivalence fun x y : T ⟶ X => ∃ φ : T ⟶ R, φ ≫ s = x ∧ φ ≫ t = y)
    (T : Scheme.{u}) :
    _root_.Equivalence fun x y : T ⟶ W.toScheme =>
      ∃ φ : T ⟶ (s ⁻¹ᵁ W).toScheme, φ ≫ sW s W = x ∧ φ ≫ tW s t W hinv = y := by
  have E := hequiv T
  exact
    { refl := fun x => (rel_restrict_iff s t W hinv x x).2 (E.refl _)
      symm := fun h => (rel_restrict_iff s t W hinv _ _).2 (E.symm ((rel_restrict_iff s t W hinv _
        _).1 h))
      trans := fun h h' => (rel_restrict_iff s t W hinv _ _).2
        (E.trans ((rel_restrict_iff s t W hinv _ _).1 h) ((rel_restrict_iff s t W hinv _ _).1 h')) }
theorem

main

L130 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_quotient_of_finiteLocallyFree_equivalenceRelation.Q1SCH.main
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace Q1SCH
Lean source · full declaration
theorem main {X R : Scheme.{u}} (s t : R ⟶ X)
    [IsFinite s] [Flat s] [LocallyOfFinitePresentation s]
    [IsFinite t] [Flat t] [LocallyOfFinitePresentation t]
    (hmono : ∀ {T : Scheme.{u}} (a b : T ⟶ R), a ≫ s = b ≫ s → a ≫ t = b ≫ t → a = b)
    (hequiv : ∀ T : Scheme.{u},
      _root_.Equivalence fun x y : T ⟶ X => ∃ φ : T ⟶ R, φ ≫ s = x ∧ φ ≫ t = y)
    (haff : ∀ x : X, ∃ U : X.Opens, IsAffineOpen U ∧ ∀ r : R, s r = x → t r ∈ U) :
    ∃ (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)) := by
  obtain ⟨W, hW, hxW, hinv⟩ := exists_invariant_affine_cover s t hequiv haff
  have loc : ∀ x : X, ∃ (Y : Scheme.{u}) (_ : IsAffine Y) (p : (W x).toScheme ⟶ Y)
      (w : sW s (W x) ≫ p = tW s t (W x) (hinv x) ≫ p),
      IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
      IsPullback (sW s (W x)) (tW s t (W x) (hinv x)) p p ∧ Nonempty (IsColimit (Cofork.ofπ p w)) :=
    fun x => by
      have : IsAffine (W x).toScheme := hW x
      have := tW_finite s t (W x) (hinv x)
      have := tW_flat s t (W x) (hinv x)
      have := tW_lfp s t (W x) (hinv x)
      exact
        AlgebraicGeometry.Scheme.exists_affine_quotient_of_finiteLocallyFree_equivalenceRelation
        (sW s (W x)) (tW s t (W x) (hinv x))
        (fun a b h₁ h₂ => mono_restrict s t (W x) (hinv x) hmono a b h₁ h₂)
        (equivalence_restrict s t (W x) (hinv x) hequiv)
  refine AlgebraicGeometry.Scheme.exists_quotient_of_forall_exists_quotient_restrict s t W hxW hinv
    fun x => ?_
  obtain ⟨Y, _, p, w, h₁, h₂, h₃, h₄, h₅, -⟩ := loc x
  exact ⟨Y, p, w, h₁, h₂, h₃, h₄, h₅⟩
theorem

exists_quotient_of_finiteLocallyFree_equivalenceRelation

L162 ↗
AlgebraicGeometry.Scheme.exists_quotient_of_finiteLocallyFree_equivalenceRelation
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_quotient_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
Lean source · full declaration
theorem _root_.AlgebraicGeometry.Scheme.exists_quotient_of_finiteLocallyFree_equivalenceRelation
    {X R : Scheme.{u}} (s t : R ⟶ X)
    [IsFinite s] [Flat s] [LocallyOfFinitePresentation s]
    [IsFinite t] [Flat t] [LocallyOfFinitePresentation t]
    (hmono : ∀ {T : Scheme.{u}} (a b : T ⟶ R), a ≫ s = b ≫ s → a ≫ t = b ≫ t → a = b)
    (hequiv : ∀ T : Scheme.{u},
      _root_.Equivalence fun x y : T ⟶ X => ∃ φ : T ⟶ R, φ ≫ s = x ∧ φ ≫ t = y)
    (haff : ∀ x : X, ∃ U : X.Opens, IsAffineOpen U ∧ ∀ r : R, s r = x → t r ∈ U) :
    ∃ (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)) :=
  Q1SCH.main s t hmono hequiv haff

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