NYLL
Module

Scheme_Modules_IsInvertible_isIso_of_locallySurjective.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_isIso_of_locallySurjective
14 declarations indexed from sourceView source ↗

Module documentation

Locally surjective maps between invertible module sheaves

A locally surjective morphism between invertible module sheaves is an isomorphism, using unit-module maps under local trivializations and a covering criterion.

Imports3
Imported by6

Declarations

def

lbF_restrictTrivOfLE

L51 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isIso_of_locallySurjective.AlgebraicGeometry.Scheme.Modules.lbF_restrictTrivOfLE
Documentation

Restricts a given trivialization to a smaller open subset.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isIso_of_locallySurjective
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
def lbF_restrictTrivOfLE {L : X.Modules} {U W : X.Opens} (h : W ≤ U)
    (e : (Modules.pullback U.ι).obj L ≅ SheafOfModules.unit U.toScheme.ringCatSheaf) :
    L.restrict W.ι ≅ (SheafOfModules.unit W.toScheme.ringCatSheaf : W.toScheme.Modules)
abbrev

lbF_unitModule

L75 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isIso_of_locallySurjective.AlgebraicGeometry.Scheme.Modules.lbF_unitModule
Documentation

The structure sheaf as a module over itself.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isIso_of_locallySurjective
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {W : Scheme.{u}}
Lean source · statement
abbrev lbF_unitModule (W : Scheme.{u}) : W.Modules
def

lbF_toSec

L80 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isIso_of_locallySurjective.AlgebraicGeometry.Scheme.Modules.lbF_toSec
Documentation

Views a section of the structure sheaf as a section of its unit module.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isIso_of_locallySurjective
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {W : Scheme.{u}}
local notation "𝒪[" W "]" => lbF_unitModule W
Lean source · statement
def lbF_toSec (U : W.Opens) : Γ(W, U) → Γ(𝒪[W], U)
def

lbF_ofSec

L83 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isIso_of_locallySurjective.AlgebraicGeometry.Scheme.Modules.lbF_ofSec
Documentation

Views a section of the unit module as a section of the structure sheaf.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isIso_of_locallySurjective
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {W : Scheme.{u}}
local notation "𝒪[" W "]" => lbF_unitModule W
Lean source · statement
def lbF_ofSec (U : W.Opens) : Γ(𝒪[W], U) → Γ(W, U)
lemma

lbF_ofSec_toSec

L85 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isIso_of_locallySurjective.AlgebraicGeometry.Scheme.Modules.lbF_ofSec_toSec
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isIso_of_locallySurjective
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {W : Scheme.{u}}
local notation "𝒪[" W "]" => lbF_unitModule W
Lean source · statement
lemma lbF_ofSec_toSec (U : W.Opens) (r : Γ(W, U)) : lbF_ofSec U (lbF_toSec U r) = r
lemma

lbF_toSec_ofSec

L87 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isIso_of_locallySurjective.AlgebraicGeometry.Scheme.Modules.lbF_toSec_ofSec
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isIso_of_locallySurjective
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {W : Scheme.{u}}
local notation "𝒪[" W "]" => lbF_unitModule W
Lean source · statement
lemma lbF_toSec_ofSec (U : W.Opens) (m : Γ(𝒪[W], U)) : lbF_toSec U (lbF_ofSec U m) =
    m
lemma

lbF_ofSec_injective

L89 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isIso_of_locallySurjective.AlgebraicGeometry.Scheme.Modules.lbF_ofSec_injective
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isIso_of_locallySurjective
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {W : Scheme.{u}}
local notation "𝒪[" W "]" => lbF_unitModule W
Lean source · statement
lemma lbF_ofSec_injective (U : W.Opens) : Function.Injective (lbF_ofSec (W := W) U)
lemma

lbF_ofSec_map

L91 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isIso_of_locallySurjective.AlgebraicGeometry.Scheme.Modules.lbF_ofSec_map
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isIso_of_locallySurjective
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {W : Scheme.{u}}
local notation "𝒪[" W "]" => lbF_unitModule W
Lean source · statement
lemma lbF_ofSec_map (U V : W.Opens) (i : V ≤ U) (m : Γ(𝒪[W], U)) :
    lbF_ofSec V ((𝒪[W]).presheaf.map (homOfLE i).op m) = W.presheaf.map (homOfLE i).op (lbF_ofSec U
        m)
lemma

lbF_ofSec_app_smul

L96 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isIso_of_locallySurjective.AlgebraicGeometry.Scheme.Modules.lbF_ofSec_app_smul
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isIso_of_locallySurjective
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {W : Scheme.{u}}
local notation "𝒪[" W "]" => lbF_unitModule W
Lean source · statement
lemma lbF_ofSec_app_smul (ψ : 𝒪[W] ⟶ 𝒪[W]) (U : W.Opens) (r : Γ(W, U)) (m : Γ(𝒪[W], U)) :
    lbF_ofSec U (ψ.app U (r • m)) = r * lbF_ofSec U (ψ.app U m)
lemma

lbF_smul_toSec_one

L100 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isIso_of_locallySurjective.AlgebraicGeometry.Scheme.Modules.lbF_smul_toSec_one
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isIso_of_locallySurjective
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {W : Scheme.{u}}
local notation "𝒪[" W "]" => lbF_unitModule W
Lean source · statement
lemma lbF_smul_toSec_one (U : W.Opens) (r : Γ(W, U)) : r • lbF_toSec U 1 = lbF_toSec U r
theorem

lbF_unitEndo_isIso_of_locallySurjective

L103 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isIso_of_locallySurjective.AlgebraicGeometry.Scheme.Modules.lbF_unitEndo_isIso_of_locallySurjective
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isIso_of_locallySurjective
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {W : Scheme.{u}}
local notation "𝒪[" W "]" => lbF_unitModule W
Lean source · statement
theorem lbF_unitEndo_isIso_of_locallySurjective (ψ : 𝒪[W] ⟶ 𝒪[W])
    (hψ : ∀ (U : W.Opens) (s : Γ(𝒪[W], U)), ∀ x ∈ U, ∃ (V : W.Opens) (i : V ≤ U),
      x ∈ V ∧ (𝒪[W]).presheaf.map (homOfLE i).op s ∈ Set.range (ψ.app V)) :
    IsIso ψ
theorem

lbF_isIso_of_isIso_app_of_iSup_eq_top

L165 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isIso_of_locallySurjective.AlgebraicGeometry.Scheme.Modules.lbF_isIso_of_isIso_app_of_iSup_eq_top
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isIso_of_locallySurjective
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
theorem lbF_isIso_of_isIso_app_of_iSup_eq_top {X : Scheme.{u}} {M N : X.Modules} (φ : M ⟶ N) {ι :
  Type v}
    (U : ι → X.Opens) (hU : ⨆ i, U i = ⊤)
    (h : ∀ (i : ι) (V : X.Opens), V ≤ U i → IsIso (φ.app V)) : IsIso φ
theorem

isIso_of_locallySurjective'

L205 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isIso_of_locallySurjective.AlgebraicGeometry.Scheme.Modules.IsInvertible.isIso_of_locallySurjective'
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isIso_of_locallySurjective
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
open scoped _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible in
Lean source · statement
theorem IsInvertible.isIso_of_locallySurjective' {L L' : X.Modules}
    (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L') (φ : L ⟶ L')
    (hφ : ∀ (U : X.Opens) (s : Γ(L', U)), ∀ x ∈ U, ∃ (V : X.Opens) (i : V ≤ U),
      x ∈ V ∧ L'.presheaf.map (homOfLE i).op s ∈ Set.range (φ.app V)) : IsIso φ
theorem

isIso_of_locallySurjective

L336 ↗
AlgebraicGeometry.Scheme.Modules.IsInvertible.isIso_of_locallySurjective
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isIso_of_locallySurjective
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible.isIso_of_locallySurjective
    {X : Scheme.{u}} {L L' : X.Modules} (hL : Scheme.Modules.IsInvertible L)
    (hL' : Scheme.Modules.IsInvertible L') (φ : L ⟶ L')
    (hφ : ∀ (U : X.Opens) (s : Γ(L', U)), ∀ x ∈ U, ∃ (V : X.Opens) (i : V ≤ U),
      x ∈ V ∧ L'.presheaf.map (homOfLE i).op s ∈ Set.range (φ.app V)) : IsIso φ

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