NYLL
Module

Scheme_Modules_exists_forall_eq_mul_of_presentations.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_forall_eq_mul_of_presentations
6 declarations indexed from sourceView source ↗

Module documentation

Uniqueness of presentations in the function field

Two compatible injective function-field presentations of the same module differ by multiplication by a single nonzero rational function on an integral scheme.

Imports3
  • Mathlib.AlgebraicGeometry.FunctionField
  • Mathlib.AlgebraicGeometry.Modules.Sheaf
  • Mathlib.Tactic.Ring.RingNF
Imported by4

Declarations

theorem

map_ne_zero

L50 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_forall_eq_mul_of_presentations.AlgebraicGeometry.Scheme.Modules.PresUniq.map_ne_zero
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_forall_eq_mul_of_presentations
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace PresUniq
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
variable {X : Scheme.{u}} [IsIntegral X] (M : X.Modules)
Lean source · statement
theorem map_ne_zero (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
    (hnat : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V → ∀ m : Γ(M, U), φ V (M.presheaf.map
        (homOfLE h).op m) = φ U m)
    (hinj : ∀ U : X.Opens, Nonempty U → Function.Injective (φ U))
    {U V : X.Opens} (h : V ≤ U) [hV : Nonempty V] {m : Γ(M, U)} (hm : m ≠ 0) :
    M.presheaf.map (homOfLE h).op m ≠ 0
theorem

ratio_eq_of_affine

L62 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_forall_eq_mul_of_presentations.AlgebraicGeometry.Scheme.Modules.PresUniq.ratio_eq_of_affine
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_forall_eq_mul_of_presentations
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace PresUniq
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
variable {X : Scheme.{u}} [IsIntegral X] (M : X.Modules)
Lean source · statement
theorem ratio_eq_of_affine (φ φ' : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
    (hsmul : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
      φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
    (hsmul' : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
      φ' U (a • m) = algebraMap Γ(X, U) X.functionField a * φ' U m)
    (hinj : ∀ U : X.Opens, Nonempty U → Function.Injective (φ U))
    (U : X.Opens) (hU : IsAffineOpen U) [Nonempty U] (m₁ m₂ : Γ(M, U)) (h₁ : m₁ ≠ 0) (h₂ : m₂ ≠ 0) :
    φ' U m₁ / φ U m₁ = φ' U m₂ / φ U m₂
theorem

ratio_eq

L121 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_forall_eq_mul_of_presentations.AlgebraicGeometry.Scheme.Modules.PresUniq.ratio_eq
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_forall_eq_mul_of_presentations
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace PresUniq
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
variable {X : Scheme.{u}} [IsIntegral X] (M : X.Modules)
variable (φ φ' : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hnat : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V → ∀ m : Γ(M, U), φ V (M.presheaf.map
      (homOfLE h).op m) = φ U m)
  (hnat' : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V → ∀ m : Γ(M, U), φ' V (M.presheaf.map
      (homOfLE h).op m) = φ' U m)
  (hsmul : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
  (hsmul' : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ' U (a • m) = algebraMap Γ(X, U) X.functionField a * φ' U m)
  (hinj : ∀ U : X.Opens, Nonempty U → Function.Injective (φ U))
  (hinj' : ∀ U : X.Opens, Nonempty U → Function.Injective (φ' U))
include hnat hnat' hsmul hsmul' hinj in
Lean source · statement
theorem ratio_eq (U₁ U₂ : X.Opens) [Nonempty U₁] [Nonempty U₂] (m₁ : Γ(M, U₁)) (m₂ : Γ(M, U₂))
    (h₁ : m₁ ≠ 0) (h₂ : m₂ ≠ 0) :
    φ' U₁ m₁ / φ U₁ m₁ = φ' U₂ m₂ / φ U₂ m₂
theorem

exists_eq_mul

L138 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_forall_eq_mul_of_presentations.AlgebraicGeometry.Scheme.Modules.PresUniq.exists_eq_mul
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_forall_eq_mul_of_presentations
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace PresUniq
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
variable {X : Scheme.{u}} [IsIntegral X] (M : X.Modules)
variable (φ φ' : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
  (hnat : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V → ∀ m : Γ(M, U), φ V (M.presheaf.map
      (homOfLE h).op m) = φ U m)
  (hnat' : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V → ∀ m : Γ(M, U), φ' V (M.presheaf.map
      (homOfLE h).op m) = φ' U m)
  (hsmul : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
  (hsmul' : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
    φ' U (a • m) = algebraMap Γ(X, U) X.functionField a * φ' U m)
  (hinj : ∀ U : X.Opens, Nonempty U → Function.Injective (φ U))
  (hinj' : ∀ U : X.Opens, Nonempty U → Function.Injective (φ' U))
include hnat hnat' hsmul hsmul' hinj hinj' in
Lean source · statement
theorem exists_eq_mul (U₀ : X.Opens) [Nonempty U₀] (m₀ : Γ(M, U₀)) (hm₀ : m₀ ≠ 0) :
    ∃ g : X.functionField, g ≠ 0 ∧ ∀ (U : X.Opens) [Nonempty U] (m : Γ(M, U)), φ' U m = g * φ U
        m
theorem

exists_forall_eq_mul_of_presentations'

L163 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_forall_eq_mul_of_presentations.AlgebraicGeometry.Scheme.Modules.exists_forall_eq_mul_of_presentations'
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_forall_eq_mul_of_presentations
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open scoped AlgebraicGeometry _root_.AlgebraicGeometry.Scheme
    _root_.AlgebraicGeometry.Scheme.Modules in
open AlgebraicGeometry.Scheme.Modules.PresUniq in
Lean source · statement
theorem AlgebraicGeometry.Scheme.Modules.exists_forall_eq_mul_of_presentations'
    {X : Scheme.{u}} [IsIntegral X] (M : X.Modules)
    (φ φ' : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
    (hnat : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
      ∀ m : Γ(M, U), φ V (M.presheaf.map (homOfLE h).op m) = φ U m)
    (hnat' : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
      ∀ m : Γ(M, U), φ' V (M.presheaf.map (homOfLE h).op m) = φ' U m)
    (hsmul : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
      φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
    (hsmul' : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
      φ' U (a • m) = algebraMap Γ(X, U) X.functionField a * φ' U m)
    (hinj : ∀ U : X.Opens, Nonempty U → Function.Injective (φ U))
    (hinj' : ∀ U : X.Opens, Nonempty U → Function.Injective (φ' U))
    (hsec : ∃ (U : X.Opens) (m : Γ(M, U)), m ≠ 0) :
    ∃ g : X.functionField, g ≠ 0 ∧ ∀ (U : X.Opens) [Nonempty U] (m : Γ(M, U)), φ' U m = g * φ U
        m
theorem

exists_forall_eq_mul_of_presentations

L197 ↗
AlgebraicGeometry.Scheme.Modules.exists_forall_eq_mul_of_presentations
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_forall_eq_mul_of_presentations
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open AlgebraicGeometry.Scheme.Modules.PresUniq in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.exists_forall_eq_mul_of_presentations
    {X : Scheme.{u}} [IsIntegral X] (M : X.Modules)
    (φ φ' : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
    (hnat : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
      ∀ m : Γ(M, U), φ V (M.presheaf.map (homOfLE h).op m) = φ U m)
    (hnat' : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
      ∀ m : Γ(M, U), φ' V (M.presheaf.map (homOfLE h).op m) = φ' U m)
    (hsmul : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
      φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
    (hsmul' : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
      φ' U (a • m) = algebraMap Γ(X, U) X.functionField a * φ' U m)
    (hinj : ∀ U : X.Opens, Nonempty U → Function.Injective (φ U))
    (hinj' : ∀ U : X.Opens, Nonempty U → Function.Injective (φ' U))
    (hsec : ∃ (U : X.Opens) (m : Γ(M, U)), m ≠ 0) :
    ∃ g : X.functionField, g ≠ 0 ∧ ∀ (U : X.Opens) [Nonempty U] (m : Γ(M, U)), φ' U m = g * φ U m

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