Module

Scheme_Modules_FiniteBySections_of_iso.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_FiniteBySections_of_iso

3 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Finite By Sections of iso

Imports2

Imported by6

theorem

map_app

L34 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_iso.FBSIsoSketch.map_app

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_iso
universe u
open CategoryTheory AlgebraicGeometry Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace FBSIsoSketch
variable {X : Scheme.{u}} {M M' : X.Modules}

Lean source · statement

theorem map_app (φ : M ⟶ M') {U V : X.Opens} (i : V ⟶ U) (s : Γ(M, U)) :
    M'.presheaf.map i.op (φ.app U s) = φ.app V (M.presheaf.map i.op s)

theorem

app_bijective

L40 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_iso.FBSIsoSketch.app_bijective

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_iso
universe u
open CategoryTheory AlgebraicGeometry Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace FBSIsoSketch
variable {X : Scheme.{u}} {M M' : X.Modules}

Lean source · statement

theorem app_bijective (e : M ≅ M') (U : X.Opens) : Function.Bijective (e.hom.app U)

theorem

of_iso

L46 ↗

AlgebraicGeometry.Scheme.Modules.FiniteBySections.of_iso

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_iso
universe u
open CategoryTheory AlgebraicGeometry Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
open FBSIsoSketch in

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.FiniteBySections.of_iso
    {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {M M' : X.Modules} (e : M ≅
      M')
    (hM : M.FiniteBySections f) : M'.FiniteBySections f

Module documentation

Scheme Modules Finite By Sections of iso

Declarations

map_app

app_bijective

of_iso