Module

Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation

19 declarations indexed from sourceView source ↗

Module documentation

Scheme exists invariant is Affine Open of finite Locally Free equivalence Relation

Imports63

Mathlib.Algebra.Algebra.Defs
Mathlib.Algebra.Category.Ring.Basic
Mathlib.Algebra.Group.Units.Basic
Mathlib.Algebra.Group.Units.Defs
Mathlib.Algebra.GroupWithZero.Units.Basic
Mathlib.Algebra.Module.Equiv.Basic
Mathlib.Algebra.Module.LinearMap.Defs
Mathlib.Algebra.Module.Projective
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Morphisms.Affine
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Mathlib.AlgebraicGeometry.Morphisms.Flat
Mathlib.AlgebraicGeometry.Morphisms.Integral
Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.AlgebraicGeometry.Scheme
Mathlib.CategoryTheory.Category.Basic
Mathlib.CategoryTheory.Category.Preorder
Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Mathlib.Data.Finset.Defs
Mathlib.Data.Fintype.Defs
Mathlib.Data.Set.Basic
Mathlib.Data.Set.Finite.Basic
Mathlib.Data.Set.Lattice.Bounded
Mathlib.LinearAlgebra.Charpoly.BaseChange
Mathlib.LinearAlgebra.Determinant
Mathlib.LinearAlgebra.FreeModule.Basic
Mathlib.LinearAlgebra.StdBasis
Mathlib.LinearAlgebra.TensorProduct.Basis
Mathlib.LinearAlgebra.TensorProduct.Defs
Mathlib.LinearAlgebra.TensorProduct.Tower
Mathlib.Logic.Equiv.Defs
Mathlib.RingTheory.FinitePresentation
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.Finiteness.Cardinality
Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Mathlib.RingTheory.Flat.EquationalCriterion
Mathlib.RingTheory.Ideal.Lattice
Mathlib.RingTheory.Ideal.Maximal
Mathlib.RingTheory.Ideal.Nonunits
Mathlib.RingTheory.Ideal.Operations
Mathlib.RingTheory.LocalRing.ResidueField.Defs
Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Mathlib.RingTheory.RingHom.Flat
Mathlib.RingTheory.Spectrum.Prime.Basic
Mathlib.RingTheory.Spectrum.Prime.Defs
Mathlib.RingTheory.Spectrum.Prime.RingHom
Mathlib.RingTheory.Spectrum.Prime.Topology
Mathlib.RingTheory.TensorProduct.Basic
Mathlib.RingTheory.TensorProduct.Finite
Mathlib.Tactic.Abel
Mathlib.Tactic.Set
Mathlib.Topology.Basic
Mathlib.Topology.Closure
Mathlib.Topology.Continuous
Mathlib.Topology.Sets.Opens

Imported by2

def

cls

L96 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation.Q1NBHD.cls

Documentation

The equivalence class of a point under the given relation.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
open scoped TensorProduct
universe u
namespace Q1NBHD
variable {X R : Scheme.{u}} (s t : R ⟶ X)

Lean source · statement

def cls (w : X) : Set X

theorem

mem_cls_self

L104 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation.Q1NBHD.mem_cls_self

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
open scoped TensorProduct
universe u
namespace Q1NBHD
variable {X R : Scheme.{u}} (s t : R ⟶ X)
section points
variable (hequiv : ∀ T : Scheme.{u},
  _root_.Equivalence fun x y : T ⟶ X => ∃ φ : T ⟶ R, φ ≫ s = x ∧ φ ≫ t = y)
include hequiv

Lean source · statement

theorem mem_cls_self (w : X) : w ∈ cls s t w

theorem

exists_inv

L110 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation.Q1NBHD.exists_inv

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
open scoped TensorProduct
universe u
namespace Q1NBHD
variable {X R : Scheme.{u}} (s t : R ⟶ X)
section points
variable (hequiv : ∀ T : Scheme.{u},
  _root_.Equivalence fun x y : T ⟶ X => ∃ φ : T ⟶ R, φ ≫ s = x ∧ φ ≫ t = y)
include hequiv

Lean source · statement

theorem exists_inv (r : R) : ∃ r' : R, s r' = t r ∧ t r' = s r

theorem

cls_symm

L114 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation.Q1NBHD.cls_symm

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
open scoped TensorProduct
universe u
namespace Q1NBHD
variable {X R : Scheme.{u}} (s t : R ⟶ X)
section points
variable (hequiv : ∀ T : Scheme.{u},
  _root_.Equivalence fun x y : T ⟶ X => ∃ φ : T ⟶ R, φ ≫ s = x ∧ φ ≫ t = y)
include hequiv

Lean source · statement

theorem cls_symm {w w' : X} (h : w' ∈ cls s t w) : w ∈ cls s t w'

theorem

cls_trans

L119 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation.Q1NBHD.cls_trans

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
open scoped TensorProduct
universe u
namespace Q1NBHD
variable {X R : Scheme.{u}} (s t : R ⟶ X)
section points
variable (hequiv : ∀ T : Scheme.{u},
  _root_.Equivalence fun x y : T ⟶ X => ∃ φ : T ⟶ R, φ ≫ s = x ∧ φ ≫ t = y)
include hequiv

Lean source · statement

theorem cls_trans {w w' w'' : X} (h : w' ∈ cls s t w) (h' : w'' ∈ cls s t w') : w'' ∈ cls s t w

theorem

cls_eq_of_mem

L133 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation.Q1NBHD.cls_eq_of_mem

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
open scoped TensorProduct
universe u
namespace Q1NBHD
variable {X R : Scheme.{u}} (s t : R ⟶ X)
section points
variable (hequiv : ∀ T : Scheme.{u},
  _root_.Equivalence fun x y : T ⟶ X => ∃ φ : T ⟶ R, φ ≫ s = x ∧ φ ≫ t = y)
include hequiv

Lean source · statement

theorem cls_eq_of_mem {w w' : X} (h : w' ∈ cls s t w) : cls s t w' = cls s t w

def

W'

L147 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation.Q1NBHD.W'

Documentation

The open complement of the image of the complement of the relation restricted to the chosen open.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
open scoped TensorProduct
universe u
namespace Q1NBHD
variable {X R : Scheme.{u}} (s t : R ⟶ X)
section S1
variable [IsFinite t] (U : X.Opens)

Lean source · statement

def W' : X.Opens

theorem

mem_W'_iff

L152 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation.Q1NBHD.mem_W'_iff

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
open scoped TensorProduct
universe u
namespace Q1NBHD
variable {X R : Scheme.{u}} (s t : R ⟶ X)
section S1
variable [IsFinite t] (U : X.Opens)

Lean source · statement

theorem mem_W'_iff (w : X) : w ∈ W' s t U ↔ ∀ z : R, t z = w → s z ∈ U ∧ t z ∈ U

theorem

W'_le

L166 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation.Q1NBHD.W'_le

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
open scoped TensorProduct
universe u
namespace Q1NBHD
variable {X R : Scheme.{u}} (s t : R ⟶ X)
section S1
variable [IsFinite t] (U : X.Opens)
variable (hequiv : ∀ T : Scheme.{u},
  _root_.Equivalence fun x y : T ⟶ X => ∃ φ : T ⟶ R, φ ≫ s = x ∧ φ ≫ t = y)
include hequiv

Lean source · statement

theorem W'_le : W' s t U ≤ U

theorem

cls_subset_W'

L175 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation.Q1NBHD.cls_subset_W'

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
open scoped TensorProduct
universe u
namespace Q1NBHD
variable {X R : Scheme.{u}} (s t : R ⟶ X)
section S1
variable [IsFinite t] (U : X.Opens)
variable (hequiv : ∀ T : Scheme.{u},
  _root_.Equivalence fun x y : T ⟶ X => ∃ φ : T ⟶ R, φ ≫ s = x ∧ φ ≫ t = y)
include hequiv

Lean source · statement

theorem cls_subset_W' {x : X} (hx : cls s t x ⊆ (U : Set X)) : cls s t x ⊆ (W' s t U : Set X)

theorem

preimage_W'_le

L184 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation.Q1NBHD.preimage_W'_le

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
open scoped TensorProduct
universe u
namespace Q1NBHD
variable {X R : Scheme.{u}} (s t : R ⟶ X)
section S1
variable [IsFinite t] (U : X.Opens)
variable (hequiv : ∀ T : Scheme.{u},
  _root_.Equivalence fun x y : T ⟶ X => ∃ φ : T ⟶ R, φ ≫ s = x ∧ φ ≫ t = y)
include hequiv

Lean source · statement

theorem preimage_W'_le : s ⁻¹ᵁ W' s t U ≤ t ⁻¹ᵁ U

theorem

exists_norm

L199 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation.Q1NBHD.exists_norm

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
open scoped TensorProduct
universe u
namespace Q1NBHD
variable {X R : Scheme.{u}} (s t : R ⟶ X)
section S4
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B] [Module.Finite A B]
  [Module.Projective A B]

Lean source · statement

theorem exists_norm : ∃ N : B → A, ∀ (b : B) (p : PrimeSpectrum A),
    N b ∉ p.asIdeal ↔ ∀ q : PrimeSpectrum B, q.comap (algebraMap A B) = p → b ∉ q.asIdeal

theorem

exists_basicOpen_of_finite

L302 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation.Q1NBHD.exists_basicOpen_of_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_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
open scoped TensorProduct
universe u
namespace Q1NBHD
variable {X R : Scheme.{u}} (s t : R ⟶ X)

Lean source · statement

theorem exists_basicOpen_of_finite {X : Scheme.{u}} {U : X.Opens} (hU : IsAffineOpen U)
    (F : Set X) (hF : F.Finite) (V : X.Opens) (hFV : F ⊆ (V : Set X)) (hFU : F ⊆ (U : Set X)) :
    ∃ f : Γ(X, U), F ⊆ (X.basicOpen f : Set X) ∧ X.basicOpen f ≤ V

theorem

mem_basicOpen_iff_notMem

L365 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation.Q1NBHD.mem_basicOpen_iff_notMem

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
open scoped TensorProduct
universe u
namespace Q1NBHD
variable {X R : Scheme.{u}} (s t : R ⟶ X)
section core
variable {X R : Scheme.{u}} (s t : R ⟶ X) [IsFinite s] [Flat s] [LocallyOfFinitePresentation s]

Lean source · statement

theorem mem_basicOpen_iff_notMem {U : X.Opens} (hU : IsAffineOpen U) (g : Γ(X, U)) {w : X}
    (hw : w ∈ U) : w ∈ X.basicOpen g ↔ g ∉ (hU.primeIdealOf ⟨w, hw⟩).asIdeal

theorem

fromSpec_mem

L374 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation.Q1NBHD.fromSpec_mem

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
open scoped TensorProduct
universe u
namespace Q1NBHD
variable {X R : Scheme.{u}} (s t : R ⟶ X)
section core
variable {X R : Scheme.{u}} (s t : R ⟶ X) [IsFinite s] [Flat s] [LocallyOfFinitePresentation s]

Lean source · statement

theorem fromSpec_mem {U : X.Opens} (hU : IsAffineOpen U) (p : PrimeSpectrum Γ(X, U)) :
    hU.fromSpec p ∈ U

theorem

primeIdealOf_fromSpec

L379 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation.Q1NBHD.primeIdealOf_fromSpec

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
open scoped TensorProduct
universe u
namespace Q1NBHD
variable {X R : Scheme.{u}} (s t : R ⟶ X)
section core
variable {X R : Scheme.{u}} (s t : R ⟶ X) [IsFinite s] [Flat s] [LocallyOfFinitePresentation s]

Lean source · statement

theorem primeIdealOf_fromSpec {U : X.Opens} (hU : IsAffineOpen U) (p : PrimeSpectrum Γ(X, U)) :
    hU.primeIdealOf ⟨hU.fromSpec p, fromSpec_mem hU p⟩ = p

theorem

exists_basicOpen_forall

L384 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation.Q1NBHD.exists_basicOpen_forall

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
open scoped TensorProduct
universe u
namespace Q1NBHD
variable {X R : Scheme.{u}} (s t : R ⟶ X)
section core
variable {X R : Scheme.{u}} (s t : R ⟶ X) [IsFinite s] [Flat s] [LocallyOfFinitePresentation s]

Lean source · statement

theorem exists_basicOpen_forall {U : X.Opens} (f : Γ(X, U)) (hD : IsAffineOpen (X.basicOpen f))
    (hVU : s ⁻¹ᵁ X.basicOpen f ≤ t ⁻¹ᵁ U) :
    ∃ g : Γ(X, X.basicOpen f), ∀ w : X, w ∈ X.basicOpen f →
      (w ∈ X.basicOpen g ↔ ∀ r : R, s r = w → t r ∈ X.basicOpen f)

theorem

main

L444 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation.Q1NBHD.main

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
open scoped TensorProduct
universe u
namespace Q1NBHD
variable {X R : Scheme.{u}} (s t : R ⟶ X)

Lean source · full declaration

theorem main [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)
    {x : X} {U : X.Opens} (hU : IsAffineOpen U) (hx : ∀ r : R, s r = x → t r ∈ U) :
    ∃ W : X.Opens, IsAffineOpen W ∧ x ∈ W ∧ W ≤ U ∧ s ⁻¹ᵁ W = t ⁻¹ᵁ W := by
  have hcls : cls s t x ⊆ (U : Set X) := by
    rintro _ ⟨r, hr, rfl⟩; exact hx r hr
  have hfin : (cls s t x).Finite := by
    have : cls s t x = t.base '' (s.base ⁻¹' {x}) := by
      ext w; simp only [cls, Set.mem_ofPred_eq, Set.mem_image, Set.mem_preimage,
        Set.mem_singleton_iff]
    rw [this]
    exact (s.finite_preimage_singleton x).image _
  obtain ⟨f, hfcls, hfW'⟩ := exists_basicOpen_of_finite hU (cls s t x) hfin (W' s t U)
    (cls_subset_W' s t U hequiv hcls) hcls
  have hD : IsAffineOpen (X.basicOpen f) := hU.basicOpen f
  have hVU : s ⁻¹ᵁ X.basicOpen f ≤ t ⁻¹ᵁ U :=
    le_trans (Scheme.Hom.preimage_mono s hfW') (preimage_W'_le s t U hequiv)
  obtain ⟨g, hg⟩ := exists_basicOpen_forall s t f hD hVU
  refine ⟨X.basicOpen g, hD.basicOpen g, ?_, ?_, ?_⟩
  · have hxD : x ∈ X.basicOpen f := hfcls (mem_cls_self s t hequiv x)
    rw [hg x hxD]
    intro r hr
    exact hfcls ⟨r, hr, rfl⟩
  · exact le_trans (X.basicOpen_le g) (le_trans (X.basicOpen_le f) le_rfl)
  · have hW : ∀ w : X, w ∈ X.basicOpen g ↔ cls s t w ⊆ (X.basicOpen f : Set X) := fun w => by
      constructor
      · intro hw
        have hwD : w ∈ X.basicOpen f := X.basicOpen_le g hw
        rw [hg w hwD] at hw
        rintro _ ⟨r, hr, rfl⟩
        exact hw r hr
      · intro hsub
        have hwD : w ∈ X.basicOpen f := hsub (mem_cls_self s t hequiv w)
        rw [hg w hwD]
        intro r hr
        exact hsub ⟨r, hr, rfl⟩
    ext r
    change s r ∈ X.basicOpen g ↔ t r ∈ X.basicOpen g
    rw [hW, hW, cls_eq_of_mem s t hequiv (⟨r, rfl, rfl⟩ : t r ∈ cls s t (s r))]

theorem

exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation

L499 ↗

AlgebraicGeometry.Scheme.exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicGeometry.Scheme
universe u
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open Scheme_exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation in
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace in
open scoped TensorProduct in

Lean source · full declaration

theorem exists_invariant_isAffineOpen_of_finiteLocallyFree_equivalenceRelation
    {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)
    {x : X} {U : X.Opens} (hU : IsAffineOpen U) (hx : ∀ r : R, s r = x → t r ∈ U) :
    ∃ W : X.Opens, IsAffineOpen W ∧ x ∈ W ∧ W ≤ U ∧ s ⁻¹ᵁ W = t ⁻¹ᵁ W :=
  Q1NBHD.main s t hequiv hU hx

Module documentation

Scheme exists invariant is Affine Open of finite Locally Free equivalence Relation

Declarations