NYLL
Module

Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
37 declarations indexed from sourceView source ↗

Module documentation

Scheme Two Affine Open Cover exists basic Open refinement basis pushforward

Imports57
Imported by3

Declarations

def

Bmod

L124 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Dict.Bmod
Documentation

The target ring viewed as the underlying type of its module over the source ring.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
namespace EXREF
namespace Dict
open _root_.AlgebraicGeometry
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
def Bmod (_φ : A ⟶ B) : Type u
instance

(anonymous instance)

L125 ↗
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
namespace EXREF
namespace Dict
open _root_.AlgebraicGeometry
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
instance : CommRing (Bmod φ)
instance

algB

L126 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Dict.algB
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
namespace EXREF
namespace Dict
open _root_.AlgebraicGeometry
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
instance algB : Algebra A (Bmod φ)
lemma

algebraMap_Bmod

L128 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Dict.algebraMap_Bmod
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
namespace EXREF
namespace Dict
open _root_.AlgebraicGeometry
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
lemma algebraMap_Bmod (a : A) : algebraMap A (Bmod φ) a = (φ.hom a : B)
theorem

finite_Bmod

L130 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Dict.finite_Bmod
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
namespace EXREF
namespace Dict
open _root_.AlgebraicGeometry
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
theorem finite_Bmod [IsFinite (Spec.map φ)] : Module.Finite A (Bmod φ)
theorem

flat_Bmod

L134 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Dict.flat_Bmod
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
namespace EXREF
namespace Dict
open _root_.AlgebraicGeometry
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
theorem flat_Bmod [Flat (Spec.map φ)] : Module.Flat A (Bmod φ)
theorem

finitePresentation_Bmod

L138 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Dict.finitePresentation_Bmod
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
namespace EXREF
namespace Dict
open _root_.AlgebraicGeometry
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
theorem finitePresentation_Bmod [IsFinite (Spec.map φ)] [LocallyOfFinitePresentation (Spec.map φ)] :
    Module.FinitePresentation A (Bmod φ)
theorem

finrank_Bmod

L145 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Dict.finrank_Bmod
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
namespace EXREF
namespace Dict
open _root_.AlgebraicGeometry
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
theorem finrank_Bmod [IsFinite (Spec.map φ)] [Flat (Spec.map φ)] (n : ℕ)
    (hn : ∀ p : Spec A, (Spec.map φ).finrank p = n)
    (K : Type u) [Field K] [Algebra A K] : Module.finrank K (K ⊗[A] Bmod φ) = n
abbrev

chartMap

L173 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Dict.chartMap
Documentation

The map on sections from an open chart to its inverse image.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
namespace EXREF
namespace Dict
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}} (π : Y ⟶ X)
Lean source · statement
abbrev chartMap (U : X.Opens) : Γ(X, U) ⟶ Γ(Y, π ⁻¹ᵁ U)
theorem

chartMap_apply

L175 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Dict.chartMap_apply
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
namespace EXREF
namespace Dict
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}} (π : Y ⟶ X)
Lean source · statement
theorem chartMap_apply (U : X.Opens) (a : Γ(X, U)) : chartMap π U a = π.app U a
theorem

isPullback_chart

L178 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Dict.isPullback_chart
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
namespace EXREF
namespace Dict
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}} (π : Y ⟶ X)
Lean source · statement
theorem isPullback_chart {U : X.Opens} (hU : IsAffineOpen U) [IsAffineHom π] :
    IsPullback (hU.preimage π).fromSpec (Spec.map (chartMap π U)) π hU.fromSpec
def

sectionsEquiv

L188 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Dict.sectionsEquiv
Documentation

The linear equivalence identifying sections of the pushed-forward unit module with the restricted-scalar module.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
namespace EXREF
namespace Dict
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}} (π : Y ⟶ X)
Lean source · full declaration
def sectionsEquiv (U : X.Opens) :
    Γ((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules), U) ≃ₗ[Γ(X, U)] Bmod (chartMap π U) where
  toFun s := (show Γ(Y, π ⁻¹ᵁ U) from s)
  invFun b := (show Γ((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules), U) from (show Γ(Y, π ⁻¹ᵁ
    U) from b))
  map_add' _ _ := rfl
  map_smul' a s := by
    change π.app U a * (show Γ(Y, π ⁻¹ᵁ U) from s) = (chartMap π U) a * (show Γ(Y, π ⁻¹ᵁ U) from s)
    rw [chartMap_apply]
  left_inv _ := rfl
  right_inv _ := rfl
theorem

finite_sections_pushforward_unit

L200 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Dict.finite_sections_pushforward_unit
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
namespace EXREF
namespace Dict
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}} (π : Y ⟶ X)
Lean source · statement
theorem finite_sections_pushforward_unit [IsFinite π] {U : X.Opens} (hU : IsAffineOpen U) :
    Module.Finite Γ(X, U) Γ((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules), U)
theorem

flat_sections_pushforward_unit

L207 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Dict.flat_sections_pushforward_unit
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
namespace EXREF
namespace Dict
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}} (π : Y ⟶ X)
Lean source · statement
theorem flat_sections_pushforward_unit [IsAffineHom π] [Flat π] {U : X.Opens} (hU : IsAffineOpen U)
  :
    Module.Flat Γ(X, U) Γ((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules), U)
theorem

projective_sections_pushforward_unit

L215 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Dict.projective_sections_pushforward_unit
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
namespace EXREF
namespace Dict
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}} (π : Y ⟶ X)
Lean source · statement
theorem projective_sections_pushforward_unit [IsFinite π] [Flat π] [LocallyOfFinitePresentation π]
    {U : X.Opens} (hU : IsAffineOpen U) :
    Module.Projective Γ(X, U) Γ((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules), U)
theorem

finrank_baseChange_sections_pushforward_unit

L230 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Dict.finrank_baseChange_sections_pushforward_unit
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
namespace EXREF
namespace Dict
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}} (π : Y ⟶ X)
Lean source · statement
theorem finrank_baseChange_sections_pushforward_unit [IsFinite π] [Flat π]
  [LocallyOfFinitePresentation π]
    (d : ℕ) (hd : ∀ x : X, π.finrank x = d) {U : X.Opens} (hU : IsAffineOpen U)
    (K : Type u) [Field K] [Algebra Γ(X, U) K] :
    Module.finrank K (K ⊗[Γ(X, U)] Γ((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules), U)) = d
theorem

compl_finite_of_nonempty

L336 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Topo.compl_finite_of_nonempty
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace EXREF
namespace Topo
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
theorem compl_finite_of_nonempty
    (hX : ∀ Z : Set X, IsClosed Z → Z ≠ Set.univ → Z.Finite ∧ ∀ z ∈ Z, IsClosed ({z} : Set X))
    (O : X.Opens) (hO : (O : Set X).Nonempty) :
    ((O : Set X)ᶜ).Finite ∧ ∀ z ∈ (O : Set X)ᶜ, IsClosed ({z} : Set X)
theorem

exists_finset_isMaximal

L346 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Topo.exists_finset_isMaximal
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace EXREF
namespace Topo
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
theorem exists_finset_isMaximal {U : X.Opens} (hU : IsAffineOpen U) {T : Set X} (hT : T.Finite)
    (hTU : T ⊆ U) (hTc : ∀ z ∈ T, IsClosed ({z} : Set X)) :
    ∃ S : Finset (Ideal Γ(X, U)), (∀ 𝔭 ∈ S, 𝔭.IsMaximal) ∧
      ∀ f : Γ(X, U), (∀ 𝔭 ∈ S, f ∉ 𝔭) → T ⊆ X.basicOpen f
theorem

exists_finset_isMaximal'

L366 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Topo.exists_finset_isMaximal'
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace EXREF
namespace Topo
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
theorem exists_finset_isMaximal' {U : X.Opens} (hU : IsAffineOpen U) {Z : Set X} (hZ : IsClosed Z)
    (hfin : (Z ∩ (U : Set X)).Finite) :
    ∃ S : Finset (Ideal Γ(X, U)), (∀ 𝔭 ∈ S, 𝔭.IsMaximal) ∧
      ∀ f : Γ(X, U), (∀ 𝔭 ∈ S, f ∉ 𝔭) → Z ∩ (U : Set X) ⊆ X.basicOpen f
theorem

sup_basicOpen_eq_top

L400 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Topo.sup_basicOpen_eq_top
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace EXREF
namespace Topo
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
theorem sup_basicOpen_eq_top {U0 U1 : X.Opens} (h : U0 ⊔ U1 = ⊤) (f₀ : Γ(X, U0)) (f₁ : Γ(X, U1))
    (h₁ : ∀ x ∈ (U1 : Set X), x ∉ (U0 : Set X) → x ∈ X.basicOpen f₁)
    (h₀ : ∀ x ∈ (U0 : Set X), x ∉ X.basicOpen f₁ → x ∈ X.basicOpen f₀) :
    X.basicOpen f₀ ⊔ X.basicOpen f₁ = ⊤
def

refinedCover

L420 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Topo.refinedCover
Documentation

The two-affine-open cover obtained by replacing both charts with basic opens that still cover.

Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace EXREF
namespace Topo
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · full declaration
def refinedCover (𝒱 : X.TwoAffineOpenCover) (f₀ : Γ(X, 𝒱.U0)) (f₁ : Γ(X, 𝒱.U1))
    (hsup : X.basicOpen f₀ ⊔ X.basicOpen f₁ = ⊤) : X.TwoAffineOpenCover where
  U0 := X.basicOpen f₀
  U1 := X.basicOpen f₁
  isAffineOpen_U0 := 𝒱.isAffineOpen_U0.basicOpen f₀
  isAffineOpen_U1 := 𝒱.isAffineOpen_U1.basicOpen f₁
  sup_eq_top := hsup
  isAffineOpen_inf := by
    have e : X.basicOpen f₀ ⊓ X.basicOpen f₁ =
        X.basicOpen (X.presheaf.map (homOfLE (inf_le_left : 𝒱.U0 ⊓ 𝒱.U1 ≤ 𝒱.U0)).op f₀ *
          X.presheaf.map (homOfLE (inf_le_right : 𝒱.U0 ⊓ 𝒱.U1 ≤ 𝒱.U1)).op f₁) := by
      rw [Scheme.basicOpen_mul, Scheme.basicOpen_res, Scheme.basicOpen_res]
      apply le_antisymm
      · refine le_inf (le_inf (le_inf ?_ ?_) inf_le_left) (le_inf (le_inf ?_ ?_) inf_le_right)
        · exact inf_le_left.trans (X.basicOpen_le f₀)
        · exact inf_le_right.trans (X.basicOpen_le f₁)
        · exact inf_le_left.trans (X.basicOpen_le f₀)
        · exact inf_le_right.trans (X.basicOpen_le f₁)
      · exact le_inf (inf_le_left.trans inf_le_right) (inf_le_right.trans inf_le_right)
    rw [e]
    exact 𝒱.isAffineOpen_inf.basicOpen _
theorem

refinedCover_U0

L442 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Topo.refinedCover_U0
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace EXREF
namespace Topo
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
theorem refinedCover_U0 (𝒱 : X.TwoAffineOpenCover) (f₀ : Γ(X, 𝒱.U0)) (f₁ : Γ(X,
  𝒱.U1)) (hsup) :
    (refinedCover 𝒱 f₀ f₁ hsup).U0 = X.basicOpen f₀
theorem

refinedCover_U1

L445 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Topo.refinedCover_U1
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace EXREF
namespace Topo
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
theorem refinedCover_U1 (𝒱 : X.TwoAffineOpenCover) (f₀ : Γ(X, 𝒱.U0)) (f₁ : Γ(X,
  𝒱.U1)) (hsup) :
    (refinedCover 𝒱 f₀ f₁ hsup).U1 = X.basicOpen f₁
theorem

basicOpen_nonempty

L449 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Topo.basicOpen_nonempty
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace EXREF
namespace Topo
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
theorem basicOpen_nonempty [IsIntegral X] {U : X.Opens} (f : Γ(X, U)) (hf : f ≠ 0) :
    ((X.basicOpen f : X.Opens) : Set X).Nonempty
theorem

res_res

L574 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.Scheme.Modules.RGlue.res_res
Source context 36 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace RGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
theorem res_res {U V W : X.Opens} (h₁ : V ≤ U) (h₂ : W ≤ V) (x : Γ(M, U)) :
    M.presheaf.map (homOfLE h₂).op (M.presheaf.map (homOfLE h₁).op x) =
      M.presheaf.map (homOfLE (h₂.trans h₁)).op x
theorem

res_res'

L580 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.Scheme.Modules.RGlue.res_res'
Source context 36 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace RGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
theorem res_res' {U V W : X.Opens} (h₁ : V ≤ U) (h₂ : W ≤ V) (x : Γ(X, U)) :
    X.presheaf.map (homOfLE h₂).op (X.presheaf.map (homOfLE h₁).op x) =
      X.presheaf.map (homOfLE (h₂.trans h₁)).op x
theorem

res_sum_smul

L586 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.Scheme.Modules.RGlue.res_sum_smul
Source context 36 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace RGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
theorem res_sum_smul {U W : X.Opens} (h : W ≤ U) {d : ℕ} (c : Fin d → Γ(X, U)) (v : Fin d → Γ(M,
  U)) :
    M.presheaf.map (homOfLE h).op (∑ i, c i • v i) =
      ∑ i, X.presheaf.map (homOfLE h).op (c i) • M.presheaf.map (homOfLE h).op (v i)
abbrev

ι

L598 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.Scheme.Modules.RGlue.ι
Documentation

The type of affine open subsets contained in the given open subset.

Source context 37 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace RGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {V : X.Opens} {d : ℕ} (e : Fin d → Γ(M, V))
  (he : ∀ (W : X.Opens) (hW : W ≤ V), IsAffineOpen W →
    ∃ b : Module.Basis (Fin d) Γ(X, W) Γ(M, W), ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
Lean source · statement
abbrev ι (W : X.Opens) : Type u
theorem

cover

L600 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.Scheme.Modules.RGlue.cover
Source context 37 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace RGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {V : X.Opens} {d : ℕ} (e : Fin d → Γ(M, V))
  (he : ∀ (W : X.Opens) (hW : W ≤ V), IsAffineOpen W →
    ∃ b : Module.Basis (Fin d) Γ(X, W) Γ(M, W), ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
Lean source · statement
theorem cover (W : X.Opens) : W ≤ ⨆ i : ι W, i.1
theorem

linearIndependent

L606 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.Scheme.Modules.RGlue.linearIndependent
Source context 38 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace RGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {V : X.Opens} {d : ℕ} (e : Fin d → Γ(M, V))
  (he : ∀ (W : X.Opens) (hW : W ≤ V), IsAffineOpen W →
    ∃ b : Module.Basis (Fin d) Γ(X, W) Γ(M, W), ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
include he in
Lean source · statement
theorem linearIndependent (W : X.Opens) (hW : W ≤ V) :
    ∀ c : Fin d → Γ(X, W), ∑ i, c i • M.presheaf.map (homOfLE hW).op (e i) = 0 → c = 0
theorem

exists_coords

L624 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.Scheme.Modules.RGlue.exists_coords
Source context 38 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace RGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {V : X.Opens} {d : ℕ} (e : Fin d → Γ(M, V))
  (he : ∀ (W : X.Opens) (hW : W ≤ V), IsAffineOpen W →
    ∃ b : Module.Basis (Fin d) Γ(X, W) Γ(M, W), ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
include he in
Lean source · statement
theorem exists_coords (W : X.Opens) (hW : W ≤ V) (s : Γ(M, W)) :
    ∃ c : Fin d → Γ(X, W), ∑ i, c i • M.presheaf.map (homOfLE hW).op (e i) = s
theorem

main

L666 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.Scheme.Modules.RGlue.main
Source context 38 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace RGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {V : X.Opens} {d : ℕ} (e : Fin d → Γ(M, V))
  (he : ∀ (W : X.Opens) (hW : W ≤ V), IsAffineOpen W →
    ∃ b : Module.Basis (Fin d) Γ(X, W) Γ(M, W), ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
include he in
Lean source · statement
theorem main (W : X.Opens) (hW : W ≤ V) :
    ∃ b : Module.Basis (Fin d) Γ(X, W) Γ(M, W), ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i)
theorem

exists_basis_baseChange_of_isUnit

L797 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.EXREF.exists_basis_baseChange_of_isUnit
Source context 31 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace EXREF
section BaseChange
variable {A : Type u} [CommRing A] {P : Type v} [AddCommGroup P] [Module A P]
Lean source · statement
theorem exists_basis_baseChange_of_isUnit {d : ℕ} (f : A) (e : Fin d → P)
    (hind : LinearIndependent A e) (hspan : ∀ p : P, f • p ∈ Submodule.span A (Set.range e))
    (A' : Type w) [CommRing A'] [Algebra A A'] (hu : IsUnit (algebraMap A A' f)) :
    ∃ b : Module.Basis (Fin d) A' (A' ⊗[A] P), ∀ i, b i = (1 : A') ⊗ₜ[A] e i
theorem

he_basicOpen

L940 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Assembly.he_basicOpen
Source context 37 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace EXREF
namespace Assembly
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs
open Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry
open Scheme.Modules
variable {X Y : Scheme.{u}} (π : Y ⟶ X) (d : ℕ)
Lean source · statement
theorem he_basicOpen [IsAffineHom π] {U : X.Opens} (hU : IsAffineOpen U) {f : Γ(X, U)} {e : Fin d →
  Γ(((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules)), U)}
    (hli : LinearIndependent Γ(X, U) e)
    (hspan : ∀ p : Γ(((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules)), U), f • p ∈
      Submodule.span Γ(X, U) (Set.range e)) :
    ∀ (W : X.Opens) (hW : W ≤ X.basicOpen f),
      ∃ b : Module.Basis (Fin d) Γ(X, W) Γ(((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules)), W),
        ∀ i, b i = ((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules)).presheaf.map (homOfLE hW).op
          (((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules)).presheaf.map (homOfLE
            (X.basicOpen_le f)).op (e i))
theorem

chart_step

L970 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Assembly.chart_step
Source context 39 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace EXREF
namespace Assembly
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs
open Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry
open Scheme.Modules
variable {X Y : Scheme.{u}} (π : Y ⟶ X) (d : ℕ)
variable [IsFinite π] [Flat π] [LocallyOfFinitePresentation π] (hd : ∀ x : X, π.finrank x = d)
include hd in
Lean source · statement
theorem chart_step [IsIntegral X] {U : X.Opens} (hU : IsAffineOpen U) (hUne : (U : Set X).Nonempty)
    {Z : Set X} (hZ : IsClosed Z) (hfin : (Z ∩ (U : Set X)).Finite) :
    ∃ (f : Γ(X, U)) (e : Fin d → Γ(((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules)), U)), f ≠ 0
      ∧ Z ∩ (U : Set X) ⊆ X.basicOpen f ∧
      LinearIndependent Γ(X, U) e ∧ ∀ p : Γ(((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules)),
        U), f • p ∈ Submodule.span Γ(X, U) (Set.range e)
theorem

main

L998 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry.EXREF.Assembly.main
Source context 39 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace EXREF
namespace Assembly
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs
open Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward.AlgebraicGeometry
open Scheme.Modules
variable {X Y : Scheme.{u}} (π : Y ⟶ X) (d : ℕ)
variable [IsFinite π] [Flat π] [LocallyOfFinitePresentation π] (hd : ∀ x : X, π.finrank x = d)
include hd in
Lean source · statement
theorem main [IsIntegral X]
    (hX : ∀ Z : Set X, IsClosed Z → Z ≠ Set.univ → Z.Finite)
    (𝒱 : X.TwoAffineOpenCover) (h₀ : (𝒱.U0 : Set X).Nonempty) (h₁ : (𝒱.U1 : Set X).Nonempty) :
    ∃ (f₀ : Γ(X, 𝒱.U0)) (f₁ : Γ(X, 𝒱.U1)) (𝒱' : X.TwoAffineOpenCover),
      𝒱'.U0 = X.basicOpen f₀ ∧ 𝒱'.U1 = X.basicOpen f₁ ∧
      (∃ e : Fin d → Γ(((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules)), 𝒱'.U0),
        ∀ (W : X.Opens) (hW : W ≤ 𝒱'.U0),
          ∃ b : Module.Basis (Fin d) Γ(X, W) Γ(((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules)),
            W),
            ∀ i, b i = ((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules)).presheaf.map (homOfLE
              hW).op (e i)) ∧
      (∃ e : Fin d → Γ(((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules)), 𝒱'.U1),
        ∀ (W : X.Opens) (hW : W ≤ 𝒱'.U1),
          ∃ b : Module.Basis (Fin d) Γ(X, W) Γ(((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules)),
            W),
            ∀ i, b i = ((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules)).presheaf.map (homOfLE
              hW).op (e i))
theorem

exists_basicOpen_refinement_basis_pushforward

L1120 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.exists_basicOpen_refinement_basis_pushforward
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_basicOpen_refinement_basis_pushforward
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
Lean source · statement
theorem
  _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.exists_basicOpen_refinement_basis_pushforward
    {X Y : Scheme.{u}} (π : Y ⟶ X) [IsFinite π] [Flat π] [LocallyOfFinitePresentation π]
    (d : ℕ) (hd : ∀ x : X, π.finrank x = d)
    [IsIntegral X]
    (hX : ∀ Z : Set X, IsClosed Z → Z ≠ Set.univ → Z.Finite)
    (𝒱 : X.TwoAffineOpenCover) (h₀ : (𝒱.U0 : Set X).Nonempty) (h₁ : (𝒱.U1 : Set X).Nonempty) :
    ∃ (f₀ : Γ(X, 𝒱.U0)) (f₁ : Γ(X, 𝒱.U1)) (𝒱' : X.TwoAffineOpenCover),
      𝒱'.U0 = X.basicOpen f₀ ∧ 𝒱'.U1 = X.basicOpen f₁ ∧
      (∃ e : Fin d → Γ((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules), 𝒱'.U0),
        ∀ (W : X.Opens) (hW : W ≤ 𝒱'.U0),
          ∃ b : Module.Basis (Fin d) Γ(X, W) Γ((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules),
            W),
            ∀ i, b i = ((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules)).presheaf.map (homOfLE
              hW).op (e i)) ∧
      (∃ e : Fin d → Γ((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules), 𝒱'.U1),
        ∀ (W : X.Opens) (hW : W ≤ 𝒱'.U1),
          ∃ b : Module.Basis (Fin d) Γ(X, W) Γ((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules),
            W),
            ∀ i, b i = ((Scheme.Modules.pushforward π).obj (𝟙_ Y.Modules)).presheaf.map (homOfLE
              hW).op (e i))

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