Module

Scheme_Modules_IsInvertible_eq_of_forall_pullbackSection_eq.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_eq_of_forall_pullbackSection_eq

6 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Is Invertible eq of forall pullback Section eq

Imports5

Mathlib.Tactic.Choose
Mathlib.AlgebraicGeometry.AlgClosed.Basic
Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesSectionZeroScheme
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq

Imported by1

Nyll.AlgebraicCurves.Geometry.Sheaves.All

lemma

unitSection_eq_smul

L58 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_eq_of_forall_pullbackSection_eq.AlgebraicGeometry.R4bAux.unitSection_eq_smul

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_eq_of_forall_pullbackSection_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace R4bAux
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

lemma unitSection_eq_smul (U : X.Opens) (m : Γ(𝟙_ X.Modules, U)) :
    m = ofUnitSection U m • toUnitSection U 1

lemma

app_eq_smul

L63 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_eq_of_forall_pullbackSection_eq.AlgebraicGeometry.R4bAux.app_eq_smul

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_eq_of_forall_pullbackSection_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace R4bAux
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

lemma app_eq_smul (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens) (m : Γ(𝟙_ X.Modules, U)) :
    s.app U m = ofUnitSection U m • s.app U (toUnitSection U 1)

lemma

map_toUnitSection_one

L68 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_eq_of_forall_pullbackSection_eq.AlgebraicGeometry.R4bAux.map_toUnitSection_one

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_eq_of_forall_pullbackSection_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace R4bAux
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

lemma map_toUnitSection_one {V W : X.Opens} (i : W ⟶ V) :
    (𝟙_ X.Modules).presheaf.map i.op (toUnitSection V 1) = toUnitSection W 1

lemma

map_app_one

L73 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_eq_of_forall_pullbackSection_eq.AlgebraicGeometry.R4bAux.map_app_one

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_eq_of_forall_pullbackSection_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace R4bAux
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

lemma map_app_one {V W : X.Opens} (i : W ⟶ V) (s : 𝟙_ X.Modules ⟶ M) :
    M.presheaf.map i.op (s.app V (toUnitSection V 1)) = s.app W (toUnitSection W 1)

theorem

eq_zero_of_zeroSchemeIdeal_eq_bot

L79 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_eq_of_forall_pullbackSection_eq.AlgebraicGeometry.R4bAux.eq_zero_of_zeroSchemeIdeal_eq_bot

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_eq_of_forall_pullbackSection_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace R4bAux
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

theorem eq_zero_of_zeroSchemeIdeal_eq_bot (hM : Scheme.Modules.IsInvertible M) (s : 𝟙_ X.Modules ⟶
  M)
    (hZ : zeroSchemeIdeal s = ⊥) : s = 0

theorem

eq_of_forall_pullbackSection_eq

L123 ↗

AlgebraicGeometry.Scheme.Modules.IsInvertible.eq_of_forall_pullbackSection_eq

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_eq_of_forall_pullbackSection_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open AlgebraicGeometry.R4bAux in

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible.eq_of_forall_pullbackSection_eq
    {k : Type u} [Field k] [IsAlgClosed k] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of k))
    [LocallyOfFiniteType f] [IsReduced X]
    {L : X.Modules} (hL : Scheme.Modules.IsInvertible L) (σ₁ σ₂ : 𝟙_ X.Modules ⟶ L)
    (h : ∀ p : Spec (CommRingCat.of k) ⟶ X, p ≫ f = 𝟙 _ →
      Scheme.Modules.pullbackSection p σ₁ = Scheme.Modules.pullbackSection p σ₂) :
    σ₁ = σ₂

Module documentation

Scheme Modules Is Invertible eq of forall pullback Section eq

Declarations

unitSection_eq_smul

app_eq_smul

map_toUnitSection_one

map_app_one

eq_zero_of_zeroSchemeIdeal_eq_bot

eq_of_forall_pullbackSection_eq