Module

StructureSheafSectionsEquiv.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.StructureSheafSectionsEquiv

2 declarations indexed from sourceView source ↗

Module documentation

The coefficient-preserving section equivalence of an actual unit isomorphism

Evaluation of the sheaf isomorphism gives the native section-module equivalence. Restriction of scalars uses the existing base-ring action and its existing scalar tower.

Imports2

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCechSectionsOf
Mathlib.Algebra.Category.ModuleCat.Basic

Imported by1

Nyll.EtaleFundamentalGroups.FiniteEtale.All

def

structureSheafSectionsEquiv

L28 ↗

AlgebraicGeometry.structureSheafSectionsEquiv

Documentation

The actual section equivalence induced by an isomorphism with the structure sheaf, with the original affine base-ring action.

Source context 4 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u

Lean source · full declaration

def structureSheafSectionsEquiv
    {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R))
    (M : X.Modules) (e : M ≅ SheafOfModules.unit X.ringCatSheaf) :
    let : Algebra R Γ(X, ⊤) := Scheme.TwoAffineOpenCover.algebraOfHom f ⊤
    let : Module R Γ(M, ⊤) := Scheme.TwoAffineOpenCover.moduleSectionsOfHom f M ⊤
    Γ(M, ⊤) ≃ₗ[R] Γ(X, ⊤) := by
  intro hRX hRM
  have hTower : IsScalarTower R Γ(X, ⊤) Γ(M, ⊤) :=
    Scheme.TwoAffineOpenCover.isScalarTower_sections f M ⊤
  let eΓ : Γ(M, ⊤) ≃ₗ[Γ(X, ⊤)] Γ(X, ⊤) :=
    (((SheafOfModules.forget X.ringCatSheaf) ⋙
      PresheafOfModules.evaluation X.ringCatSheaf.obj (Opposite.op ⊤)).mapIso e).toLinearEquiv
  exact eΓ.restrictScalars R

theorem

structureSheafSectionsEquiv_apply

L43 ↗

AlgebraicGeometry.structureSheafSectionsEquiv_apply