Module

Scheme_Modules_IsInvertible_zeroSchemeIdeal_eq_of_app_eq_smul.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_zeroSchemeIdeal_eq_of_app_eq_smul

4 declarations indexed from sourceView source ↗

Module documentation

Unit multiples give the same zero-scheme ideal

Global sections of an invertible module related by multiplication by a unit have the same zero-scheme ideal.

Imports2

Imported by5

theorem

map_app_unit

L41 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_zeroSchemeIdeal_eq_of_app_eq_smul.ZSWs13.map_app_unit

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

Lean source · statement

theorem map_app_unit (φ : 𝟙_ X.Modules ⟶ M) {U V : X.Opens} (i : U ⟶ V)
    (m : Γ(𝟙_ X.Modules, V)) :
    M.presheaf.map i.op (φ.app V m) = φ.app U ((𝟙_ X.Modules).presheaf.map i.op m)

theorem

map_toUnitSection_one

L49 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_zeroSchemeIdeal_eq_of_app_eq_smul.ZSWs13.map_toUnitSection_one

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

Lean source · statement

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

theorem

app_one_eq_map

L56 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_zeroSchemeIdeal_eq_of_app_eq_smul.ZSWs13.app_one_eq_map

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

Lean source · statement

theorem app_one_eq_map (φ : 𝟙_ X.Modules ⟶ M) (U : X.Opens) :
    φ.app U (Scheme.Modules.toUnitSection U 1) =
      M.presheaf.map (homOfLE (le_top : U ≤ ⊤)).op (φ.app ⊤ (Scheme.Modules.toUnitSection ⊤ 1))

theorem

zeroSchemeIdeal_eq_of_app_eq_smul

L65 ↗

AlgebraicGeometry.Scheme.Modules.IsInvertible.zeroSchemeIdeal_eq_of_app_eq_smul

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_zeroSchemeIdeal_eq_of_app_eq_smul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
open ZSWs13 in

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible.zeroSchemeIdeal_eq_of_app_eq_smul
    {X : Scheme.{u}} {M : X.Modules} (hM : Scheme.Modules.IsInvertible M)
    (s₁ s₂ : 𝟙_ X.Modules ⟶ M) (u : Γ(X, ⊤)) (hu : IsUnit u)
    (h : s₂.app ⊤ (Scheme.Modules.toUnitSection ⊤ 1) = u • s₁.app ⊤
        (Scheme.Modules.toUnitSection ⊤ 1)) :
    Scheme.Modules.zeroSchemeIdeal s₁ = Scheme.Modules.zeroSchemeIdeal s₂

Module documentation

Unit multiples give the same zero-scheme ideal

Declarations

map_app_unit

map_toUnitSection_one

app_one_eq_map

zeroSchemeIdeal_eq_of_app_eq_smul