NYLL
Module

Scheme_Modules_IsLocallyFreeOfRank_exists_basis.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
28 declarations indexed from sourceView source ↗

Module documentation

Local bases of finite locally free module sheaves

Local trivializations yield compatible bases of section modules on smaller opens contained in a neighborhood of each point.

Imports1
Imported by8

Declarations

def

piPowAb

L41 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.PresheafOfModules.piPowAb
Documentation

The presheaf of finite tuples of ring sections.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
variable {C : Type*} [Category C] (R : Cᵒᵖ ⥤ CommRingCat.{u}) (n : ℕ)
Lean source · full declaration
def piPowAb : Cᵒᵖ ⥤ Ab.{u} where
  obj X := AddCommGrpCat.of (Fin n → R.obj X)
  map {X Y} f := AddCommGrpCat.ofHom (AddMonoidHom.compLeft (R.map f).hom.toAddMonoidHom (Fin n))
  map_id X := by ext v i; simp
  map_comp f g := by ext v i; simp
instance

instModulePiPowAb

L47 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.PresheafOfModules.instModulePiPowAb
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
variable {C : Type*} [Category C] (R : Cᵒᵖ ⥤ CommRingCat.{u}) (n : ℕ)
Lean source · statement
instance instModulePiPowAb (X : Cᵒᵖ) :
    Module ((R ⋙ forget₂ CommRingCat RingCat).obj X) ((piPowAb R n).obj X)
def

piPow

L52 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.PresheafOfModules.piPow
Documentation

The module presheaf of finite tuples of ring sections.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
variable {C : Type*} [Category C] (R : Cᵒᵖ ⥤ CommRingCat.{u}) (n : ℕ)
Lean source · statement
def piPow : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat)
lemma

piPow_map_apply

L58 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.PresheafOfModules.piPow_map_apply
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
variable {C : Type*} [Category C] (R : Cᵒᵖ ⥤ CommRingCat.{u}) (n : ℕ)
Lean source · full declaration
lemma piPow_map_apply {X Y : Cᵒᵖ} (f : X ⟶ Y) (v : Fin n → R.obj X) (i : Fin n) :
    ((piPow R n).map f (show (piPow R n).obj X from v) : Fin n → R.obj Y) i = R.map f (v i) := rfl
lemma

piPow_map_basisFun

L61 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.PresheafOfModules.piPow_map_basisFun
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
variable {C : Type*} [Category C] (R : Cᵒᵖ ⥤ CommRingCat.{u}) (n : ℕ)
Lean source · full declaration
lemma piPow_map_basisFun {X Y : Cᵒᵖ} (f : X ⟶ Y) (j : Fin n) :
    ((piPow R n).map f (show (piPow R n).obj X from Pi.basisFun (R.obj X) (Fin n) j) :
      Fin n → R.obj Y) = Pi.basisFun (R.obj Y) (Fin n) j := by
  funext i
  rw [piPow_map_apply, Pi.basisFun_apply, Pi.basisFun_apply, Pi.single_apply, Pi.single_apply]
  split_ifs <;> simp
lemma

sum_app

L74 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.PresheafOfModules.sum_app
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
Lean source · statement
lemma sum_app {C : Type*} [Category C] {R : Cᵒᵖ ⥤ RingCat.{u}} {M N : PresheafOfModules.{u} R}
    {ι : Type*} (s : Finset ι) (f : ι → (M ⟶ N)) (X : Cᵒᵖ) :
    (∑ i ∈ s, f i).app X = ∑ i ∈ s, (f i).app X
lemma

sum_val

L85 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.SheafOfModules.sum_val
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace SheafOfModules
open _root_.SheafOfModules
open _root_.SheafOfModules
Lean source · statement
lemma sum_val {C : Type*} [Category C] {J : GrothendieckTopology C} {R : Sheaf J RingCat.{u}}
    {M N : SheafOfModules.{u} R} {ι : Type*} (s : Finset ι) (f : ι → (M ⟶ N)) :
    (∑ i ∈ s, f i).val = ∑ i ∈ s, (f i).val
abbrev

piPowPresheaf

L107 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.AlgebraicGeometry.Scheme.Modules.piPowPresheaf
Documentation

The tuple module presheaf over the scheme structure ring.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
Lean source · statement
abbrev piPowPresheaf : X.PresheafOfModules
abbrev

ringCatSheafAb

L110 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.AlgebraicGeometry.Scheme.Modules.ringCatSheafAb
Documentation

The additive sheaf underlying the structure ring.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
Lean source · statement
abbrev ringCatSheafAb : Sheaf (Opens.grothendieckTopology X) AddCommGrpCat.{u}
def

piPowCone

L115 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.AlgebraicGeometry.Scheme.Modules.piPowCone
Documentation

The product cone whose coordinates are the structure sheaf.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
Lean source · full declaration
def piPowCone :
    Cone (Discrete.functor (fun _ : Fin n => ringCatSheafAb X) ⋙ sheafToPresheaf _ _) where
  pt := (piPowPresheaf X n).presheaf
  π := Discrete.natTrans (fun i =>
    { app := fun V => AddCommGrpCat.ofHom (X := Fin n → (X.presheaf.obj V : Type u))
        (Y := (X.presheaf.obj V : Type u))
        (Pi.evalAddMonoidHom (fun _ : Fin n => (X.presheaf.obj V : Type u)) i.as)
      naturality := fun V W g => by ext v; rfl })
def

isLimitPiPowCone

L125 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.AlgebraicGeometry.Scheme.Modules.isLimitPiPowCone
Documentation

The universal property of the finite tuple product cone.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
Lean source · statement
def isLimitPiPowCone : IsLimit (piPowCone X n)
lemma

isSheaf_piPowPresheaf

L140 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.AlgebraicGeometry.Scheme.Modules.isSheaf_piPowPresheaf
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
Lean source · statement
lemma isSheaf_piPowPresheaf :
    Presheaf.IsSheaf (Opens.grothendieckTopology X) (piPowPresheaf X n).presheaf
def

piPow

L144 ↗
AlgebraicGeometry.Scheme.Modules.piPow
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
Lean source · full declaration
def _root_.AlgebraicGeometry.Scheme.Modules.piPow : X.Modules where
  val := piPowPresheaf X n
  isSheaf := isSheaf_piPowPresheaf X n
def

piPowπ

L151 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.AlgebraicGeometry.Scheme.Modules.piPowπ
Documentation

Projection of the tuple module sheaf onto one coordinate.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
open _root_.AlgebraicGeometry.Scheme.Modules
Lean source · statement
def piPowπ (i : Fin n) : piPow X n ⟶ SheafOfModules.unit X.ringCatSheaf
lemma

piPowπ_apply

L159 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.AlgebraicGeometry.Scheme.Modules.piPowπ_apply
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
open _root_.AlgebraicGeometry.Scheme.Modules
Lean source · full declaration
lemma piPowπ_apply (i : Fin n) (V : X.Opensᵒᵖ) (v : Fin n → (X.presheaf.obj V : Type u)) :
    ((piPowπ X n i).val.app V (show (piPow X n).val.obj V from v) : X.presheaf.obj V) = v i := rfl
def

piPowι

L163 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.AlgebraicGeometry.Scheme.Modules.piPowι
Documentation

Insertion of a structure-sheaf section into one tuple coordinate.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
open _root_.AlgebraicGeometry.Scheme.Modules
Lean source · statement
def piPowι (i : Fin n) : SheafOfModules.unit X.ringCatSheaf ⟶ piPow X n
lemma

piPowι_apply

L182 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.AlgebraicGeometry.Scheme.Modules.piPowι_apply
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
open _root_.AlgebraicGeometry.Scheme.Modules
Lean source · full declaration
lemma piPowι_apply (i : Fin n) (V : X.Opensᵒᵖ) (a : (X.presheaf.obj V : Type u)) :
    ((piPowι X n i).val.app V (show (SheafOfModules.unit X.ringCatSheaf).val.obj V from a) :
      Fin n → X.presheaf.obj V) = Pi.single i a := rfl
def

piPowBicone

L187 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.AlgebraicGeometry.Scheme.Modules.piPowBicone
Documentation

The finite biproduct bicone of copies of the structure module.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
open _root_.AlgebraicGeometry.Scheme.Modules
Lean source · full declaration
def piPowBicone :
    Bicone (fun _ : ULift.{u} (Fin n) => SheafOfModules.unit X.ringCatSheaf) where
  pt := piPow X n
  π j := piPowπ X n j.down
  ι j := piPowι X n j.down
  ι_π j j' := by
    refine SheafOfModules.hom_ext (PresheafOfModules.hom_ext fun V => ModuleCat.hom_ext
      (LinearMap.ext fun (a : X.presheaf.obj V) => ?_))
    by_cases h : j = j'
    · subst h
      rw [dite_eq_left rfl]
      change (Pi.single j.down a : Fin n → X.presheaf.obj V) j.down = a
      simp
    · rw [dite_eq_right h]
      have h' : j'.down ≠ j.down := fun e => h (ULift.ext e.symm)
      change (Pi.single j.down a : Fin n → X.presheaf.obj V) j'.down = (0 : X.presheaf.obj V)
      simp [h']
lemma

piPowBicone_total

L205 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.AlgebraicGeometry.Scheme.Modules.piPowBicone_total
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
open _root_.AlgebraicGeometry.Scheme.Modules
Lean source · statement
lemma piPowBicone_total :
    ∑ j : ULift.{u} (Fin n), (piPowBicone X n).π j ≫ (piPowBicone X n).ι j = 𝟙 (piPow X n)
def

isBilimitPiPowBicone

L221 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.AlgebraicGeometry.Scheme.Modules.isBilimitPiPowBicone
Documentation

The bilimit structure on the finite tuple bicone.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
open _root_.AlgebraicGeometry.Scheme.Modules
Lean source · statement
def isBilimitPiPowBicone : (piPowBicone X n).IsBilimit
def

freeIsoPiPow

L225 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.AlgebraicGeometry.Scheme.Modules.freeIsoPiPow
Documentation

The comparison between the finite free module sheaf and its tuple model.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
open _root_.AlgebraicGeometry.Scheme.Modules
Lean source · statement
def freeIsoPiPow : SheafOfModules.free.{u} (ULift.{u} (Fin n)) ≅ piPow X n
lemma

map_eq_map'

L246 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.AlgebraicGeometry.Scheme.Modules.map_eq_map'
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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}}
section helpers
Lean source · statement
lemma map_eq_map' {M : X.Modules} {W₁ W₂ : X.Opens} (i j : W₁ ⟶ W₂) (m : Γ(M, W₂)) :
    M.presheaf.map i.op m = M.presheaf.map j.op m
lemma

map_map_of_eq

L250 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.AlgebraicGeometry.Scheme.Modules.map_map_of_eq
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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}}
section helpers
Lean source · statement
lemma map_map_of_eq {M : X.Modules} {W₁ W₂ : X.Opens} (h : W₁ = W₂) (m : Γ(M, W₂)) :
    M.presheaf.map (homOfLE h.ge).op (M.presheaf.map (homOfLE h.le).op m) = m
lemma

ringMap_ringMap_of_eq

L258 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.AlgebraicGeometry.Scheme.Modules.ringMap_ringMap_of_eq
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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}}
section helpers
Lean source · statement
lemma ringMap_ringMap_of_eq {W₁ W₂ : X.Opens} (h : W₁ = W₂) (a : Γ(X, W₂)) :
    X.presheaf.map (homOfLE h.ge).op (X.presheaf.map (homOfLE h.le).op a) = a
lemma

image_preimage_eq_of_le

L266 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.AlgebraicGeometry.Scheme.Modules.image_preimage_eq_of_le
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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}}
section helpers
Lean source · statement
lemma image_preimage_eq_of_le {V W : X.Opens} (hW : W ≤ V) : V.ι ''ᵁ (V.ι ⁻¹ᵁ W) = W
lemma

restrictFunctor_obj_presheaf_map

L269 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis.AlgebraicGeometry.Scheme.Modules.restrictFunctor_obj_presheaf_map
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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}}
section helpers
Lean source · statement
lemma restrictFunctor_obj_presheaf_map (M : X.Modules) (V : X.Opens) {W₁ W₂ : (V :
  Scheme.{u}).Opens}
    (i : W₁ ⟶ W₂) (m : Γ((restrictFunctor V.ι).obj M, W₂)) :
    ((restrictFunctor V.ι).obj M).presheaf.map i.op m =
      M.presheaf.map (homOfLE (V.ι.image_mono i.le)).op (m : Γ(M, V.ι ''ᵁ W₂))
theorem

exists_basis_impl

L284 ↗
AlgebraicGeometry.Scheme.Modules.IsLocallyFreeOfRank.exists_basis_impl
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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}}
namespace IsLocallyFreeOfRank
open scoped _root_.AlgebraicGeometry.Scheme.Modules.IsLocallyFreeOfRank in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.IsLocallyFreeOfRank.exists_basis_impl {n :
    ℕ} {M : X.Modules} (hM : IsLocallyFreeOfRank n M) (x : X) :
    ∃ (V : X.Opens), x ∈ V ∧ ∃ e : Fin n → Γ(M, V), ∀ (W : X.Opens) (hW : W ≤ V),
      ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W), ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i)
theorem

exists_basis

L413 ↗
AlgebraicGeometry.Scheme.Modules.IsLocallyFreeOfRank.exists_basis
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_exists_basis
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.IsLocallyFreeOfRank.exists_basis {X :
  AlgebraicGeometry.Scheme.{u}} {n : ℕ} {M : X.Modules}
    (hM : AlgebraicGeometry.Scheme.Modules.IsLocallyFreeOfRank n M) (x : X) :
    ∃ (V : X.Opens), x ∈ V ∧ ∃ e : Fin n → Γ(M, V), ∀ (W : X.Opens) (hW : W ≤ V),
      ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W), ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i)

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