NYLL
Module

Scheme_Modules_IsInvertible_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk
10 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Is Invertible bijective presheaf map inf of is Integrally Closed stalk

Imports12
Imported by2

Declarations

lemma

map_map

L69 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.HartogsLB.map_map
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace HartogsLB
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
lemma map_map {M : X.Modules} {U V V' : X.Opens} (i : V ⟶ U) (j : V' ⟶ V) (s : Γ(M, U)) :
    M.presheaf.map j.op (M.presheaf.map i.op s) = M.presheaf.map (j ≫ i).op s
lemma

map_congr

L74 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.HartogsLB.map_congr
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace HartogsLB
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
lemma map_congr {M : X.Modules} {U V : X.Opens} (i j : V ⟶ U) (s : Γ(M, U)) :
    M.presheaf.map i.op s = M.presheaf.map j.op s
lemma

rmap_map

L78 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.HartogsLB.rmap_map
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace HartogsLB
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
lemma rmap_map {U V V' : X.Opens} (i : V ⟶ U) (j : V' ⟶ V) (g : Γ(X, U)) :
    X.presheaf.map j.op (X.presheaf.map i.op g) = X.presheaf.map (j ≫ i).op g
lemma

rmap_congr

L83 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.HartogsLB.rmap_congr
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace HartogsLB
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
lemma rmap_congr {U V : X.Opens} (i j : V ⟶ U) (g : Γ(X, U)) :
    X.presheaf.map i.op g = X.presheaf.map j.op g
def

shf

L88 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.HartogsLB.shf
Documentation

The underlying sheaf of abelian groups of a sheaf of modules.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace HartogsLB
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
def shf (M : X.Modules) : TopCat.Sheaf Ab X.carrier
lemma

map_smul_frame

L90 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.HartogsLB.map_smul_frame
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace HartogsLB
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
lemma map_smul_frame {M : X.Modules} {O W W' : X.Opens} (hWO : W ≤ O) (hW'W : W' ≤ W) (e : Γ(M, O))
    (g : Γ(X, W)) :
    M.presheaf.map (homOfLE hW'W).op (g • M.presheaf.map (homOfLE hWO).op e) =
      X.presheaf.map (homOfLE hW'W).op g • M.presheaf.map (homOfLE (hW'W.trans hWO)).op e
lemma

bijective_fun

L105 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.HartogsLB.bijective_fun
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_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace HartogsLB
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Main
variable [IsLocallyNoetherian X] (V U : X.Opens)
  (hV : ∀ x : X, x ∈ V → IsDomain (X.presheaf.stalk x) ∧ IsIntegrallyClosed (X.presheaf.stalk x))
  (hU : ∀ x : X, x ∈ V → ringKrullDim (X.presheaf.stalk x) ≤ 1 → x ∈ U)
  {L : X.Modules}
include hV hU in
Lean source · statement
lemma bijective_fun (W : X.Opens) (hWV : W ≤ V) :
    Function.Bijective (X.presheaf.map (homOfLE (inf_le_left : W ⊓ U ≤ W)).op)
lemma

injective_of_frames

L110 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.HartogsLB.injective_of_frames
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_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace HartogsLB
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Main
variable [IsLocallyNoetherian X] (V U : X.Opens)
  (hV : ∀ x : X, x ∈ V → IsDomain (X.presheaf.stalk x) ∧ IsIntegrallyClosed (X.presheaf.stalk x))
  (hU : ∀ x : X, x ∈ V → ringKrullDim (X.presheaf.stalk x) ≤ 1 → x ∈ U)
  {L : X.Modules}
include hV hU in
Lean source · statement
lemma injective_of_frames (O : X → X.Opens) (e : ∀ x, Γ(L, O x)) (hxO : ∀ x, x ∈ O x)
    (he : ∀ x, IsFrameOn (e x) (O x)) (W : X.Opens) (hWV : W ≤ V) :
    Function.Injective (L.presheaf.map (homOfLE (inf_le_left : W ⊓ U ≤ W)).op)
theorem

bijective

L143 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.HartogsLB.bijective
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_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace HartogsLB
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Main
variable [IsLocallyNoetherian X] (V U : X.Opens)
  (hV : ∀ x : X, x ∈ V → IsDomain (X.presheaf.stalk x) ∧ IsIntegrallyClosed (X.presheaf.stalk x))
  (hU : ∀ x : X, x ∈ V → ringKrullDim (X.presheaf.stalk x) ≤ 1 → x ∈ U)
  {L : X.Modules}
include hV hU in
Lean source · statement
theorem bijective (hL : IsInvertible L) :
    Function.Bijective (L.presheaf.map (homOfLE (inf_le_left : V ⊓ U ≤ V)).op)
theorem

bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk

L219 ↗
AlgebraicGeometry.Scheme.Modules.IsInvertible.bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicGeometry.Scheme.Modules.IsInvertible
universe u
open _root_.CategoryTheory _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry _root_.Opposite _root_.TopologicalSpace
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs in
open Scheme_Modules_IsInvertible_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk in
Lean source · statement
theorem bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk
    {X : Scheme.{u}} [IsLocallyNoetherian X] (V U : X.Opens)
    (hV : ∀ x : X, x ∈ V → IsDomain (X.presheaf.stalk x) ∧ IsIntegrallyClosed (X.presheaf.stalk x))
    (hU : ∀ x : X, x ∈ V → ringKrullDim (X.presheaf.stalk x) ≤ 1 → x ∈ U)
    {L : X.Modules} (hL : Scheme.Modules.IsInvertible L) :
    Function.Bijective (L.presheaf.map (homOfLE (inf_le_left : V ⊓ U ≤ V)).op)

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