NYLL
Module

FrameLocality.lean

Nyll.SchemeTheory.Modules.FrameLocality
6 declarations indexed from sourceView source ↗

Module documentation

Local bijectivity of multiplication by a section

Multiplication by a fixed global section is bijective on every open when it is bijective on a suitable neighbourhood of each point.

Imports2
  • Mathlib.AlgebraicGeometry.Modules.Sheaf
  • Mathlib.Tactic.Choose
Imported by6

Declarations

abbrev

res

L37 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_of_forall_exists_bijective_smul.FrameLocalSol.res
Documentation

The restriction of the fixed global section σ to the open subset W.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_of_forall_exists_bijective_smul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace FrameLocalSol
variable {X : Scheme.{u}} (M : X.Modules) (σ : Γ(M, ⊤))
Lean source · statement
abbrev res (W : X.Opens) : Γ(M, W)
theorem

res_map

L39 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_of_forall_exists_bijective_smul.FrameLocalSol.res_map
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_of_forall_exists_bijective_smul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace FrameLocalSol
variable {X : Scheme.{u}} (M : X.Modules) (σ : Γ(M, ⊤))
Lean source · statement
theorem res_map {W W' : X.Opens} (i : W' ⟶ W) : M.presheaf.map i.op (res M σ W) = res M σ W'
theorem

smul_res

L43 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_of_forall_exists_bijective_smul.FrameLocalSol.smul_res
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_of_forall_exists_bijective_smul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace FrameLocalSol
variable {X : Scheme.{u}} (M : X.Modules) (σ : Γ(M, ⊤))
Lean source · statement
theorem smul_res {W W' : X.Opens} (i : W' ⟶ W) (g : Γ(X, W)) :
    M.presheaf.map i.op (g • res M σ W) = X.presheaf.map i.op g • res M σ W'
def

abSheaf

L48 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_of_forall_exists_bijective_smul.FrameLocalSol.abSheaf
Documentation

The sheaf of abelian groups underlying the module sheaf M.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_of_forall_exists_bijective_smul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace FrameLocalSol
variable {X : Scheme.{u}} (M : X.Modules) (σ : Γ(M, ⊤))
Lean source · statement
def abSheaf : TopCat.Sheaf Ab X.carrier
theorem

main

L50 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_of_forall_exists_bijective_smul.FrameLocalSol.main
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_of_forall_exists_bijective_smul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace FrameLocalSol
variable {X : Scheme.{u}} (M : X.Modules) (σ : Γ(M, ⊤))
Lean source · full declaration
theorem main (V : X.Opens)
    (h : ∀ x ∈ V, ∃ U : X.Opens, x ∈ U ∧ ∀ W : X.Opens, W ≤ U →
      Function.Bijective fun g : Γ(X, W) => g • res M σ W) :
    Function.Bijective fun g : Γ(X, V) => g • res M σ V := by
  classical
  choose U hxU hU using fun x : V => h x.1 x.2
  let W : V → X.Opens := fun x => V ⊓ U x
  have hWV : ∀ x, W x ≤ V := fun x => inf_le_left
  have hWU : ∀ x, W x ≤ U x := fun x => inf_le_right
  have hcover : V ≤ iSup W := fun y hy => Opens.mem_iSup.2 ⟨⟨y, hy⟩, ⟨hy, hxU ⟨y, hy⟩⟩⟩
  constructor
  · intro g₁ g₂ hg
    have hg' : g₁ • res M σ V = g₂ • res M σ V := hg
    apply TopCat.Sheaf.eq_of_locally_eq' X.sheaf W V (fun x => homOfLE (hWV x)) hcover
    intro x
    apply (hU x (W x) (hWU x)).1
    change X.presheaf.map (homOfLE (hWV x)).op g₁ • res M σ (W x) =
      X.presheaf.map (homOfLE (hWV x)).op g₂ • res M σ (W x)
    rw [← smul_res, ← smul_res, hg']
  · intro s
    have hloc : ∀ x, ∃! g : Γ(X, W x), g • res M σ (W x) = M.presheaf.map (homOfLE (hWV x)).op s :=
      fun x => (Function.bijective_iff_existsUnique _).1 (hU x (W x) (hWU x)) _
    choose gx hgx hgx_uniq using hloc
    have hcompat : TopCat.Presheaf.IsCompatible X.sheaf.obj W gx := by
      intro x y
      apply (hU x (W x ⊓ W y) (inf_le_left.trans (hWU x))).1
      change X.presheaf.map (Opens.infLELeft (W x) (W y)).op (gx x) • res M σ (W x ⊓ W y) =
        X.presheaf.map (Opens.infLERight (W x) (W y)).op (gx y) • res M σ (W x ⊓ W y)
      rw [← smul_res M σ (Opens.infLELeft (W x) (W y)), hgx x, ← smul_res M σ (Opens.infLERight
          (W x) (W y)),
        hgx y, ← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, ← Functor.map_comp,
        ← Functor.map_comp, ← op_comp, ← op_comp]
      rfl
    obtain ⟨g, hg, -⟩ : ∃! g : Γ(X, V), ∀ x, X.presheaf.map (homOfLE (hWV x)).op g = gx x :=
      TopCat.Sheaf.existsUnique_gluing' X.sheaf W V (fun x => homOfLE (hWV x)) hcover gx hcompat
    refine ⟨g, ?_⟩
    apply TopCat.Sheaf.eq_of_locally_eq' (abSheaf M) W V (fun x => homOfLE (hWV x)) hcover
    intro x
    change M.presheaf.map (homOfLE (hWV x)).op (g • res M σ V) = M.presheaf.map (homOfLE (hWV
        x)).op s
    rw [smul_res, ← hgx x]
    exact congrArg (· • res M σ (W x)) (hg x)
theorem

bijective_smul_of_forall_exists_bijective_smul

L95 ↗
AlgebraicGeometry.Scheme.Modules.bijective_smul_of_forall_exists_bijective_smul
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_of_forall_exists_bijective_smul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
Lean source · full declaration
theorem _root_.AlgebraicGeometry.Scheme.Modules.bijective_smul_of_forall_exists_bijective_smul
    {X : Scheme.{u}} (M : X.Modules) (σ : Γ(M, ⊤)) (V : X.Opens)
    (h : ∀ x ∈ V, ∃ U : X.Opens, x ∈ U ∧ ∀ W : X.Opens, W ≤ U →
      Function.Bijective fun g : Γ(X, W) => g • (M.presheaf.map (homOfLE (le_top : W ≤ ⊤)).op σ
          : Γ(M, W))) :
    Function.Bijective fun g : Γ(X, V) => g • (M.presheaf.map (homOfLE (le_top : V ≤ ⊤)).op σ :
        Γ(M, V)) :=
  FrameLocalSol.main M σ V h

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