Module

Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation

58 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Is Invertible exists ideal Sheaf Data tensor linear Equiv of presentation

Imports6

Mathlib.AlgebraicGeometry.FunctionField
Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Nyll.AlgebraicCurves.Geometry.Picard.Functor
Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_isQuasicoherent_ofModules_of_locallyTrivial
Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_isCoherent_ofModules_of_locallyTrivial
Nyll.AlgebraicCurves.Geometry.Projective.Scheme_Modules_projective_sections_of_locallyTrivial

Imported by4

def

intLocus

L43 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.intLocus

Documentation

The submodule of sections whose scaled image under the presentation is integral.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · full declaration

def intLocus (a : A) : Submodule A P where
  carrier := {p | IsLocalization.IsInteger A (algebraMap A K a * φ p)}
  zero_mem' := by
    change IsLocalization.IsInteger A (algebraMap A K a * φ 0)
    rw [map_zero, mul_zero]; exact IsLocalization.isInteger_zero
  add_mem' {p q} hp hq := by
    change IsLocalization.IsInteger A (algebraMap A K a * φ (p + q))
    rw [map_add, mul_add]; exact IsLocalization.isInteger_add hp hq
  smul_mem' c {p} hp := by
    change IsLocalization.IsInteger A (algebraMap A K a * φ (c • p))
    rw [LinearMap.map_smul, mul_smul_comm]; exact IsLocalization.isInteger_smul hp

def

denom

L56 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.denom

Documentation

The ideal of scalars making every image of the presentation integral.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · full declaration

def denom : Ideal A where
  carrier := {a | ∀ p, IsLocalization.IsInteger A (algebraMap A K a * φ p)}
  zero_mem' p := by
    rw [map_zero, zero_mul]; exact IsLocalization.isInteger_zero
  add_mem' {a b} ha hb p := by
    rw [map_add, add_mul]; exact IsLocalization.isInteger_add (ha p) (hb p)
  smul_mem' c {a} ha p := by
    rw [smul_eq_mul, map_mul, mul_assoc, ← Algebra.smul_def]
    exact IsLocalization.isInteger_smul (ha p)

theorem

mem_denom

L66 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.mem_denom

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · statement

theorem mem_denom {a : A} : a ∈ denom φ ↔ ∀ p, IsLocalization.IsInteger A (algebraMap A K a * φ p)

theorem

mem_denom_of_span

L70 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.mem_denom_of_span

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · statement

theorem mem_denom_of_span {s : Set P} (hs : Submodule.span A s = ⊤) {a : A}
    (h : ∀ p ∈ s, IsLocalization.IsInteger A (algebraMap A K a * φ p)) : a ∈ denom φ

theorem

exists_mem_denom

L76 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.exists_mem_denom

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · statement

theorem exists_mem_denom (S : Submonoid A) [IsLocalization S K] [Module.Finite A P] :
    ∃ s ∈ S, s ∈ denom φ

def

mulMap

L85 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.mulMap

Documentation

The linear map multiplying a denominator by a section and applying the presentation.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · statement

def mulMap : ↥(denom φ) ⊗[A] P →ₗ[A] K

theorem

mulMap_tmul

L88 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.mulMap_tmul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · statement

theorem mulMap_tmul (a : denom φ) (p : P) : mulMap φ (a ⊗ₜ p) = algebraMap A K a * φ p

theorem

mulMap_injective

L91 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.mulMap_injective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · statement

theorem mulMap_injective [Module.Flat A P] (hφ : Function.Injective φ) :
    Function.Injective (mulMap φ)

theorem

isInteger_mulMap

L96 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.isInteger_mulMap

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · statement

theorem isInteger_mulMap (t : ↥(denom φ) ⊗[A] P) : IsLocalization.IsInteger A (mulMap φ t)

theorem

range_mulMap_le

L101 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.range_mulMap_le

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · statement

theorem range_mulMap_le : LinearMap.range (mulMap φ) ≤ LinearMap.range (Algebra.linearMap A K)

def

gens

L107 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.gens

Documentation

The products of denominators with images of module sections.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · statement

def gens : Set K

theorem

range_mulMap_eq_span

L109 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.range_mulMap_eq_span

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · statement

theorem range_mulMap_eq_span : LinearMap.range (mulMap φ) = Submodule.span A (gens φ)

def

numer

L120 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.numer

Documentation

The ideal of scalars whose images lie in the range of the denominator multiplication map.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · statement

def numer : Ideal A

theorem

mem_numer

L122 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.mem_numer

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · statement

theorem mem_numer {b : A} : b ∈ numer φ ↔ algebraMap A K b ∈ LinearMap.range (mulMap φ)

theorem

map_numer_eq

L124 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.map_numer_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · statement

theorem map_numer_eq :
    Submodule.map (Algebra.linearMap A K) (numer φ) = LinearMap.range (mulMap φ)

def

numerMap

L129 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.numerMap

Documentation

The algebra map restricted to the numerator ideal.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · statement

def numerMap : ↥(numer φ) →ₗ[A] K

theorem

numerMap_injective

L131 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.numerMap_injective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · statement

theorem numerMap_injective (hinj : Function.Injective (algebraMap A K)) :
    Function.Injective (numerMap φ)

theorem

range_mulMap_eq_range_numerMap

L134 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.range_mulMap_eq_range_numerMap

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · statement

theorem range_mulMap_eq_range_numerMap :
    LinearMap.range (mulMap φ) = LinearMap.range (numerMap φ)

def

equiv

L140 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.equiv

Documentation

The tensor equivalence between the denominator ideal tensored with the module and the numerator ideal.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · statement

def equiv [Module.Flat A P] (hφ : Function.Injective φ)
    (hinj : Function.Injective (algebraMap A K)) : ↥(denom φ) ⊗[A] P ≃ₗ[A] ↥(numer φ)

theorem

algebraMap_equiv

L146 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.algebraMap_equiv

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · statement

theorem algebraMap_equiv [Module.Flat A P] (hφ : Function.Injective φ)
    (hinj : Function.Injective (algebraMap A K)) (t : ↥(denom φ) ⊗[A] P) :
    algebraMap A K (equiv φ hφ hinj t : A) = mulMap φ t

theorem

numer_ne_bot

L153 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.numer_ne_bot

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Denom
variable {A K : Type*} [CommRing A] [CommRing K] [Algebra A K]
variable {P : Type*} [AddCommGroup P] [Module A P] (φ : P →ₗ[A] K)

Lean source · statement

theorem numer_ne_bot [IsDomain K] (hinj : Function.Injective (algebraMap A K))
    {s : A} (hs : s ∈ denom φ) (hs0 : s ≠ 0) {p : P} (hp : φ p ≠ 0) : numer φ ≠ ⊥

theorem

map_denom_le

L178 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.map_denom_le

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Loc
variable {A B K : Type*} [CommRing A] [CommRing B] [CommRing K]
variable [Algebra A B] [Algebra A K] [Algebra B K] [IsScalarTower A B K]
variable (f : A) [IsLocalization.Away f B]
variable {P Q : Type*} [AddCommGroup P] [Module A P] [AddCommGroup Q] [Module B Q]
variable (φP : P →ₗ[A] K) (φQ : Q →ₗ[B] K) (r : P →+ Q)
variable (hr : ∀ p, φQ (r p) = φP p)
variable (hsurj : ∀ q : Q, ∃ (n : ℕ) (p : P), r p = (algebraMap A B f ^ n) • q)
include hr hsurj in

Lean source · statement

theorem map_denom_le : (denom φP).map (algebraMap A B) ≤ denom φQ

theorem

denom_le_map

L199 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.denom_le_map

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Loc
variable {A B K : Type*} [CommRing A] [CommRing B] [CommRing K]
variable [Algebra A B] [Algebra A K] [Algebra B K] [IsScalarTower A B K]
variable (f : A) [IsLocalization.Away f B]
variable {P Q : Type*} [AddCommGroup P] [Module A P] [AddCommGroup Q] [Module B Q]
variable (φP : P →ₗ[A] K) (φQ : Q →ₗ[B] K) (r : P →+ Q)
variable (hr : ∀ p, φQ (r p) = φP p)
variable (hsurj : ∀ q : Q, ∃ (n : ℕ) (p : P), r p = (algebraMap A B f ^ n) • q)
include f hr in

Lean source · statement

theorem denom_le_map [Module.Finite A P] : denom φQ ≤ (denom φP).map (algebraMap A B)

theorem

map_denom_eq

L232 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.map_denom_eq

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Loc
variable {A B K : Type*} [CommRing A] [CommRing B] [CommRing K]
variable [Algebra A B] [Algebra A K] [Algebra B K] [IsScalarTower A B K]
variable (f : A) [IsLocalization.Away f B]
variable {P Q : Type*} [AddCommGroup P] [Module A P] [AddCommGroup Q] [Module B Q]
variable (φP : P →ₗ[A] K) (φQ : Q →ₗ[B] K) (r : P →+ Q)
variable (hr : ∀ p, φQ (r p) = φP p)
variable (hsurj : ∀ q : Q, ∃ (n : ℕ) (p : P), r p = (algebraMap A B f ^ n) • q)
include hr hsurj in

Lean source · statement

theorem map_denom_eq [Module.Finite A P] : (denom φP).map (algebraMap A B) = denom φQ

theorem

map_linearMap_map

L235 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.map_linearMap_map

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Loc
variable {A B K : Type*} [CommRing A] [CommRing B] [CommRing K]
variable [Algebra A B] [Algebra A K] [Algebra B K] [IsScalarTower A B K]
variable (f : A) [IsLocalization.Away f B]
variable {P Q : Type*} [AddCommGroup P] [Module A P] [AddCommGroup Q] [Module B Q]
variable (φP : P →ₗ[A] K) (φQ : Q →ₗ[B] K) (r : P →+ Q)
variable (hr : ∀ p, φQ (r p) = φP p)
variable (hsurj : ∀ q : Q, ∃ (n : ℕ) (p : P), r p = (algebraMap A B f ^ n) • q)

Lean source · statement

theorem map_linearMap_map (I : Ideal A) :
    Submodule.map (Algebra.linearMap B K) (I.map (algebraMap A B)) =
      Submodule.span B (algebraMap A K '' I)

theorem

range_mulMap_loc

L245 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.range_mulMap_loc

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Loc
variable {A B K : Type*} [CommRing A] [CommRing B] [CommRing K]
variable [Algebra A B] [Algebra A K] [Algebra B K] [IsScalarTower A B K]
variable (f : A) [IsLocalization.Away f B]
variable {P Q : Type*} [AddCommGroup P] [Module A P] [AddCommGroup Q] [Module B Q]
variable (φP : P →ₗ[A] K) (φQ : Q →ₗ[B] K) (r : P →+ Q)
variable (hr : ∀ p, φQ (r p) = φP p)
variable (hsurj : ∀ q : Q, ∃ (n : ℕ) (p : P), r p = (algebraMap A B f ^ n) • q)
include hr hsurj in

Lean source · statement

theorem range_mulMap_loc [Module.Finite A P] :
    LinearMap.range (mulMap φQ) = Submodule.span B (gens φP)

theorem

map_numer_eq_loc

L277 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.map_numer_eq_loc

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Loc
variable {A B K : Type*} [CommRing A] [CommRing B] [CommRing K]
variable [Algebra A B] [Algebra A K] [Algebra B K] [IsScalarTower A B K]
variable (f : A) [IsLocalization.Away f B]
variable {P Q : Type*} [AddCommGroup P] [Module A P] [AddCommGroup Q] [Module B Q]
variable (φP : P →ₗ[A] K) (φQ : Q →ₗ[B] K) (r : P →+ Q)
variable (hr : ∀ p, φQ (r p) = φP p)
variable (hsurj : ∀ q : Q, ∃ (n : ℕ) (p : P), r p = (algebraMap A B f ^ n) • q)
include hr hsurj in

Lean source · statement

theorem map_numer_eq_loc [Module.Finite A P] (hinjB : Function.Injective (algebraMap B K)) :
    (numer φP).map (algebraMap A B) = numer φQ

def

toSpecTop

L295 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.toSpecTop

Documentation

The canonical morphism to the spectrum of the ring of global sections.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}

Lean source · statement

def toSpecTop (X : Scheme.{u}) : X ⟶ Spec (.of Γ(X, ⊤))

theorem

finite_sections

L297 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.finite_sections

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}

Lean source · statement

theorem finite_sections (M : X.Modules) (hM : Scheme.Modules.IsInvertible M) (U : X.affineOpens) :
    Module.Finite Γ(X, U) Γ(M, U)

theorem

flat_sections

L301 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.flat_sections

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}

Lean source · statement

theorem flat_sections (M : X.Modules) (hM : Scheme.Modules.IsInvertible M) (U : X.affineOpens) :
    Module.Flat Γ(X, U) Γ(M, U)

theorem

res_surj

L306 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.res_surj

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}

Lean source · statement

theorem res_surj (M : X.Modules) (hM : Scheme.Modules.IsInvertible M) (U : X.affineOpens) (f : Γ(X,
  U))
    (x : Γ(M, X.basicOpen f)) :
    ∃ (n : ℕ) (y : Γ(M, U)), M.presheaf.map (homOfLE (X.basicOpen_le f)).op y =
      (X.presheaf.map (homOfLE (X.basicOpen_le f)).op).hom (f ^ n) • x

theorem

nonempty_of_le

L313 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.nonempty_of_le

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}

Lean source · statement

theorem nonempty_of_le {U V : X.Opens} (h : V ≤ U) [hV : Nonempty V] : Nonempty U

theorem

eq_bot_of_not_nonempty

L316 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.eq_bot_of_not_nonempty

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}

Lean source · statement

theorem eq_bot_of_not_nonempty {U : X.Opens} (h : ¬ Nonempty U) : U = ⊥

theorem

subsingleton_of_not_nonempty

L319 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.subsingleton_of_not_nonempty

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}

Lean source · statement

theorem subsingleton_of_not_nonempty {U : X.Opens} (h : ¬ Nonempty U) : Subsingleton Γ(X, U)

theorem

genericPoint_mem

L326 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.genericPoint_mem

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Integral
variable [AlgebraicGeometry.IsIntegral X]

Lean source · statement

theorem genericPoint_mem (U : X.Opens) [h : Nonempty U] : genericPoint X ∈ U

theorem

algebraMap_res

L329 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.algebraMap_res

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Integral
variable [AlgebraicGeometry.IsIntegral X]

Lean source · statement

theorem algebraMap_res {U V : X.Opens} [Nonempty U] [Nonempty V] (h : V ≤ U) (a : Γ(X, U)) :
    algebraMap Γ(X, V) X.functionField ((X.presheaf.map (homOfLE h).op).hom a) =
      algebraMap Γ(X, U) X.functionField a

theorem

isScalarTower_basicOpen

L334 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.isScalarTower_basicOpen

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Integral
variable [AlgebraicGeometry.IsIntegral X]

Lean source · statement

theorem isScalarTower_basicOpen (U : X.Opens) (f : Γ(X, U)) [Nonempty U] [Nonempty (X.basicOpen f)]
  :
    IsScalarTower Γ(X, U) Γ(X, X.basicOpen f) X.functionField

def

φlin

L350 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.φlin

Documentation

The function field presentation on a nonempty open viewed as a linear map over its section ring.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Families
variable [AlgebraicGeometry.IsIntegral X] (M : X.Modules)
  (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hφ₂ : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)

Lean source · full declaration

def φlin (U : X.Opens) [Nonempty U] : Γ(M, U) →ₗ[Γ(X, U)] (X.functionField : Type u) where
  toFun := φ U
  map_add' := map_add (φ U)
  map_smul' a m := by rw [RingHom.id_apply, Algebra.smul_def]; exact hφ₂ U a m

theorem

φlin_apply

L355 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.φlin_apply

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Families
variable [AlgebraicGeometry.IsIntegral X] (M : X.Modules)
  (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hφ₂ : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)

Lean source · statement

theorem φlin_apply (U : X.Opens) [Nonempty U] (m : Γ(M, U)) : φlin M φ hφ₂ U m = φ U m

def

idealI

L359 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.idealI

Documentation

The denominator ideal on each affine open, with the full ideal on an empty open.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Families
variable [AlgebraicGeometry.IsIntegral X] (M : X.Modules)
  (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hφ₂ : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
open Classical in

Lean source · statement

def idealI (U : X.affineOpens) : Ideal Γ(X, U)

def

idealJ

L364 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.idealJ

Documentation

The numerator ideal on each affine open, with the full ideal on an empty open.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Families
variable [AlgebraicGeometry.IsIntegral X] (M : X.Modules)
  (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hφ₂ : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
open Classical in

Lean source · statement

def idealJ (U : X.affineOpens) : Ideal Γ(X, U)

theorem

idealI_eq

L367 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.idealI_eq

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Families
variable [AlgebraicGeometry.IsIntegral X] (M : X.Modules)
  (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hφ₂ : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)

Lean source · statement

theorem idealI_eq (U : X.affineOpens) [h : Nonempty (U : X.Opens)] :
    idealI M φ hφ₂ U = denom (φlin M φ hφ₂ U)

theorem

idealJ_eq

L370 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.idealJ_eq

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Families
variable [AlgebraicGeometry.IsIntegral X] (M : X.Modules)
  (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hφ₂ : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)

Lean source · statement

theorem idealJ_eq (U : X.affineOpens) [h : Nonempty (U : X.Opens)] :
    idealJ M φ hφ₂ U = numer (φlin M φ hφ₂ U)

theorem

idealI_eq_top

L373 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.idealI_eq_top

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Families
variable [AlgebraicGeometry.IsIntegral X] (M : X.Modules)
  (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hφ₂ : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)

Lean source · statement

theorem idealI_eq_top (U : X.affineOpens) (h : ¬ Nonempty (U : X.Opens)) : idealI M φ hφ₂ U = ⊤

theorem

idealJ_eq_top

L376 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.idealJ_eq_top

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Families
variable [AlgebraicGeometry.IsIntegral X] (M : X.Modules)
  (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hφ₂ : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)

Lean source · statement

theorem idealJ_eq_top (U : X.affineOpens) (h : ¬ Nonempty (U : X.Opens)) : idealJ M φ hφ₂ U = ⊤

theorem

map_ideal_basicOpen

L384 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.map_ideal_basicOpen

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Families
variable [AlgebraicGeometry.IsIntegral X] (M : X.Modules)
  (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hφ₂ : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
variable (hM : Scheme.Modules.IsInvertible M)
  (hφ₁ : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
    ∀ m : Γ(M, U), φ V (M.presheaf.map (homOfLE h).op m) = φ U m)
include hM hφ₁ in

Lean source · statement

theorem map_ideal_basicOpen (U : X.affineOpens) (f : Γ(X, U)) :
    (idealI M φ hφ₂ U).map (X.presheaf.map (homOfLE <| X.basicOpen_le f).op).hom =
        idealI M φ hφ₂ (X.affineBasicOpen f) ∧
      (idealJ M φ hφ₂ U).map (X.presheaf.map (homOfLE <| X.basicOpen_le f).op).hom =
        idealJ M φ hφ₂ (X.affineBasicOpen f)

def

sheafI

L421 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.sheafI

Documentation

The ideal sheaf assembled from the denominator ideals and their basic open compatibility.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Families
variable [AlgebraicGeometry.IsIntegral X] (M : X.Modules)
  (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hφ₂ : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
variable (hM : Scheme.Modules.IsInvertible M)
  (hφ₁ : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
    ∀ m : Γ(M, U), φ V (M.presheaf.map (homOfLE h).op m) = φ U m)

Lean source · full declaration

def sheafI : X.IdealSheafData where
  ideal := idealI M φ hφ₂
  map_ideal_basicOpen U f := (map_ideal_basicOpen M φ hφ₂ hM hφ₁ U f).1

def

sheafJ

L426 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.sheafJ

Documentation

The ideal sheaf assembled from the numerator ideals and their basic open compatibility.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Families
variable [AlgebraicGeometry.IsIntegral X] (M : X.Modules)
  (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hφ₂ : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
variable (hM : Scheme.Modules.IsInvertible M)
  (hφ₁ : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
    ∀ m : Γ(M, U), φ V (M.presheaf.map (homOfLE h).op m) = φ U m)

Lean source · full declaration

def sheafJ : X.IdealSheafData where
  ideal := idealJ M φ hφ₂
  map_ideal_basicOpen U f := (map_ideal_basicOpen M φ hφ₂ hM hφ₁ U f).2

theorem

sheafI_ideal

L430 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.sheafI_ideal

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Families
variable [AlgebraicGeometry.IsIntegral X] (M : X.Modules)
  (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hφ₂ : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
variable (hM : Scheme.Modules.IsInvertible M)
  (hφ₁ : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
    ∀ m : Γ(M, U), φ V (M.presheaf.map (homOfLE h).op m) = φ U m)

Lean source · statement

theorem sheafI_ideal (U : X.affineOpens) : (sheafI M φ hφ₂ hM hφ₁).ideal U = idealI M φ hφ₂ U

theorem

sheafJ_ideal

L431 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.sheafJ_ideal

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Families
variable [AlgebraicGeometry.IsIntegral X] (M : X.Modules)
  (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hφ₂ : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
variable (hM : Scheme.Modules.IsInvertible M)
  (hφ₁ : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
    ∀ m : Γ(M, U), φ V (M.presheaf.map (homOfLE h).op m) = φ U m)

Lean source · statement

theorem sheafJ_ideal (U : X.affineOpens) : (sheafJ M φ hφ₂ hM hφ₁).ideal U = idealJ M φ hφ₂ U

theorem

exists_apply_ne_zero

L446 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.exists_apply_ne_zero

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Nonvanishing
variable [AlgebraicGeometry.IsIntegral X] (M : X.Modules) (hM : Scheme.Modules.IsInvertible M)
  (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hφ₁ : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
    ∀ m : Γ(M, U), φ V (M.presheaf.map (homOfLE h).op m) = φ U m)
  (hφ₂ : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
  (hφ₃ : ∀ U : X.Opens, Nonempty U → Function.Injective (φ U))
include hM hφ₁ hφ₂ hφ₃ in

Lean source · statement

theorem exists_apply_ne_zero (U : X.affineOpens) [Nonempty (U : X.Opens)] :
    ∃ y : Γ(M, U), φ U y ≠ 0

def

ePos

L512 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.ePos

Documentation

The denominator tensor numerator equivalence on a nonempty affine open.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Assembly
variable [AlgebraicGeometry.IsIntegral X] (M : X.Modules) (hM : Scheme.Modules.IsInvertible M)
  (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hφ₁ : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
    ∀ m : Γ(M, U), φ V (M.presheaf.map (homOfLE h).op m) = φ U m)
  (hφ₂ : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
  (hφ₃ : ∀ U : X.Opens, Nonempty U → Function.Injective (φ U))

Lean source · statement

def ePos (U : X.affineOpens) [Nonempty (U : X.Opens)] :
    ↥(idealI M φ hφ₂ U) ⊗[Γ(X, U)] Γ(M, U) ≃ₗ[Γ(X, U)] ↥(idealJ M φ hφ₂ U)

theorem

algebraMap_ePos_tmul

L520 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.algebraMap_ePos_tmul

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Assembly
variable [AlgebraicGeometry.IsIntegral X] (M : X.Modules) (hM : Scheme.Modules.IsInvertible M)
  (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hφ₁ : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
    ∀ m : Γ(M, U), φ V (M.presheaf.map (homOfLE h).op m) = φ U m)
  (hφ₂ : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
  (hφ₃ : ∀ U : X.Opens, Nonempty U → Function.Injective (φ U))

Lean source · statement

theorem algebraMap_ePos_tmul (U : X.affineOpens) [Nonempty (U : X.Opens)] (a : ↥(idealI M φ hφ₂ U))
    (m : Γ(M, U)) :
    algebraMap Γ(X, U) X.functionField (ePos M hM φ hφ₂ hφ₃ U (a ⊗ₜ m) : Γ(X, U)) =
      algebraMap Γ(X, U) X.functionField a * φ U m

def

eEmpty

L532 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.eEmpty

Documentation

The tensor equivalence on an empty affine open obtained from the subsingleton section modules.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Assembly
variable [AlgebraicGeometry.IsIntegral X] (M : X.Modules) (hM : Scheme.Modules.IsInvertible M)
  (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hφ₁ : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
    ∀ m : Γ(M, U), φ V (M.presheaf.map (homOfLE h).op m) = φ U m)
  (hφ₂ : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
  (hφ₃ : ∀ U : X.Opens, Nonempty U → Function.Injective (φ U))

Lean source · statement

def eEmpty (U : X.affineOpens) (h : ¬ Nonempty (U : X.Opens)) :
    ↥(idealI M φ hφ₂ U) ⊗[Γ(X, U)] Γ(M, U) ≃ₗ[Γ(X, U)] ↥(idealJ M φ hφ₂ U)

def

eAll

L541 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.eAll

Documentation

The tensor equivalence on every affine open, combining the nonempty and empty cases.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Assembly
variable [AlgebraicGeometry.IsIntegral X] (M : X.Modules) (hM : Scheme.Modules.IsInvertible M)
  (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hφ₁ : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
    ∀ m : Γ(M, U), φ V (M.presheaf.map (homOfLE h).op m) = φ U m)
  (hφ₂ : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
  (hφ₃ : ∀ U : X.Opens, Nonempty U → Function.Injective (φ U))
open Classical in

Lean source · statement

def eAll (U : X.affineOpens) :
    ↥(idealI M φ hφ₂ U) ⊗[Γ(X, U)] Γ(M, U) ≃ₗ[Γ(X, U)] ↥(idealJ M φ hφ₂ U)

theorem

eAll_eq

L545 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.eAll_eq

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Assembly
variable [AlgebraicGeometry.IsIntegral X] (M : X.Modules) (hM : Scheme.Modules.IsInvertible M)
  (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hφ₁ : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
    ∀ m : Γ(M, U), φ V (M.presheaf.map (homOfLE h).op m) = φ U m)
  (hφ₂ : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
  (hφ₃ : ∀ U : X.Opens, Nonempty U → Function.Injective (φ U))

Lean source · statement

theorem eAll_eq (U : X.affineOpens) [h : Nonempty (U : X.Opens)] :
    eAll M hM φ hφ₂ hφ₃ U = ePos M hM φ hφ₂ hφ₃ U

theorem

main

L549 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation.P2mDenomAlg.main

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
open TensorProduct
universe u
noncomputable section
namespace P2mDenomAlg
section Geom
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
variable {X : Scheme.{u}}
section Assembly
variable [AlgebraicGeometry.IsIntegral X] (M : X.Modules) (hM : Scheme.Modules.IsInvertible M)
  (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hφ₁ : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
    ∀ m : Γ(M, U), φ V (M.presheaf.map (homOfLE h).op m) = φ U m)
  (hφ₂ : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
  (hφ₃ : ∀ U : X.Opens, Nonempty U → Function.Injective (φ U))
include hM hφ₁ hφ₂ hφ₃ in

Lean source · statement

theorem main :
    ∃ (I J : X.IdealSheafData)
      (e : ∀ U : X.affineOpens, ↥(I.ideal U) ⊗[Γ(X, U)] Γ(M, U) ≃ₗ[Γ(X, U)] ↥(J.ideal U)),
      (∀ (U : X.affineOpens) [Nonempty U] (a : Γ(X, U)),
          a ∈ I.ideal U ↔ ∀ m : Γ(M, U), ∃ b : Γ(X, U),
            algebraMap Γ(X, U) X.functionField b = algebraMap Γ(X, U) X.functionField a * φ U m) ∧
      (∀ U : X.affineOpens, Nonempty U → I.ideal U ≠ ⊥ ∧ J.ideal U ≠ ⊥) ∧
      (∀ (U : X.affineOpens) [Nonempty U] (a : ↥(I.ideal U)) (m : Γ(M, U)),
          algebraMap Γ(X, U) X.functionField (e U (a ⊗ₜ m) : Γ(X, U)) =
            algebraMap Γ(X, U) X.functionField a * φ U m) ∧
      (∀ (U V : X.affineOpens) (h : (V : X.Opens) ≤ U) (a : ↥(I.ideal U)) (m : Γ(M, U)),
          X.presheaf.map (homOfLE h).op (e U (a ⊗ₜ m) : Γ(X, U)) =
            e V (⟨X.presheaf.map (homOfLE h).op a, I.ideal_le_comap_ideal h a.2⟩ ⊗ₜ
              M.presheaf.map (homOfLE h).op m))

theorem

exists_idealSheafData_tensor_linearEquiv_of_presentation

L620 ↗

AlgebraicGeometry.Scheme.Modules.IsInvertible.exists_idealSheafData_tensor_linearEquiv_of_presentation

Source context 7 commands

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

section ProofImplementation
section PublicStatement
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
open AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_IsInvertible_exists_idealSheafData_tensor_linearEquiv_of_presentation
namespace AlgebraicGeometry.Scheme.Modules.IsInvertible

Lean source · statement

theorem exists_idealSheafData_tensor_linearEquiv_of_presentation
    {X : Scheme.{u}} [AlgebraicGeometry.IsIntegral X] (M : X.Modules)
    (hM : Scheme.Modules.IsInvertible M)
    (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
    (hφ : (∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
          ∀ m : Γ(M, U), φ V (M.presheaf.map (homOfLE h).op m) = φ U m) ∧
      (∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
          φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m) ∧
      (∀ U : X.Opens, Nonempty U → Function.Injective (φ U))) :
    ∃ (I J : X.IdealSheafData)
      (e : ∀ U : X.affineOpens, ↥(I.ideal U) ⊗[Γ(X, U)] Γ(M, U) ≃ₗ[Γ(X, U)] ↥(J.ideal U)),
      (∀ (U : X.affineOpens) [Nonempty U] (a : Γ(X, U)),
          a ∈ I.ideal U ↔ ∀ m : Γ(M, U), ∃ b : Γ(X, U),
            algebraMap Γ(X, U) X.functionField b = algebraMap Γ(X, U) X.functionField a * φ U m) ∧
      (∀ U : X.affineOpens, Nonempty U → I.ideal U ≠ ⊥ ∧ J.ideal U ≠ ⊥) ∧
      (∀ (U : X.affineOpens) [Nonempty U] (a : ↥(I.ideal U)) (m : Γ(M, U)),
          algebraMap Γ(X, U) X.functionField (e U (a ⊗ₜ m) : Γ(X, U)) =
            algebraMap Γ(X, U) X.functionField a * φ U m) ∧
      (∀ (U V : X.affineOpens) (h : (V : X.Opens) ≤ U) (a : ↥(I.ideal U)) (m : Γ(M, U)),
          X.presheaf.map (homOfLE h).op (e U (a ⊗ₜ m) : Γ(X, U)) =
            e V (⟨X.presheaf.map (homOfLE h).op a, I.ideal_le_comap_ideal h a.2⟩ ⊗ₜ
              M.presheaf.map (homOfLE h).op m))

Module documentation

Scheme Modules Is Invertible exists ideal Sheaf Data tensor linear Equiv of presentation

Declarations