Module

Scheme_Modules_IsLocallyFreeOfRank_of_forall_exists_opens.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsLocallyFreeOfRank_of_forall_exists_opens

3 declarations indexed from sourceView source ↗

Module documentation

Local freeness from an open cover

Pullback to open subschemes identifies the local trivializations used to establish a fixed rank.

Imports2

Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesLocallyFreeOfRank

Imported by6

theorem

opensMap_final'

L43 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_of_forall_exists_opens.AlgebraicGeometry.Scheme.Modules.opensMap_final'

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsLocallyFreeOfRank_of_forall_exists_opens
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.AlgebraicGeometry.Scheme.Modules
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

Lean source · statement

theorem opensMap_final' {X Y : Scheme.{u}} (f : X ⟶ Y) :
    (TopologicalSpace.Opens.map f.base).Final

def

pullbackFreeIso'

L48 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_of_forall_exists_opens.AlgebraicGeometry.Scheme.Modules.pullbackFreeIso'

Documentation

The canonical free-module pullback identification along the final map of open-set sites.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsLocallyFreeOfRank_of_forall_exists_opens
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.AlgebraicGeometry.Scheme.Modules
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

Lean source · statement

def pullbackFreeIso' {X Y : Scheme.{u}} (f : X ⟶ Y) (I : Type u) :
    (Scheme.Modules.pullback f).obj (SheafOfModules.free.{u} I) ≅ SheafOfModules.free.{u} I

theorem

of_forall_exists_opens

L57 ↗

AlgebraicGeometry.Scheme.Modules.IsLocallyFreeOfRank.of_forall_exists_opens

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsLocallyFreeOfRank_of_forall_exists_opens
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry AlgebraicGeometry in

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.IsLocallyFreeOfRank.of_forall_exists_opens {X :
  Scheme.{u}} {n : ℕ} {M : X.Modules}
    (h : ∀ x : X, ∃ U : X.Opens, x ∈ U ∧
      Scheme.Modules.IsLocallyFreeOfRank n ((Scheme.Modules.pullback U.ι).obj M)) :
    Scheme.Modules.IsLocallyFreeOfRank n M

Module documentation

Local freeness from an open cover

Declarations

opensMap_final'

pullbackFreeIso'

of_forall_exists_opens