Module

Scheme_Modules_exists_finiteBySections_tensorPow_of_forall_geometricFibre.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_finiteBySections_tensorPow_of_forall_geometricFibre

2 declarations indexed from sourceView source ↗

Module documentation

Finite presentation by sections of tensor powers from geometric fibres

Imports13

Imported by2

def

tensorPowIso

L76 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_finiteBySections_tensorPow_of_forall_geometricFibre.W2FINSketch.tensorPowIso

Documentation

The isomorphism on tensor powers induced by an isomorphism of modules.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_finiteBySections_tensorPow_of_forall_geometricFibre
attribute [-instance]
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
  PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ
  PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η
  PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
attribute [-simp] PresheafOfModules.freeεIso_hom_app PresheafOfModules.freeμIso_hom_app
  TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply
  TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply TwoChartCech.KerCoprod.ι0_apply
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.Scheme.Modules.tensorSections_zero_right
  AlgebraicGeometry.Scheme.Modules.map_unitSection
  AlgebraicGeometry.Scheme.Modules.tensorSectionsBilin_apply
  AlgebraicGeometry.Scheme.Modules.tensorPowSection_zero
  AlgebraicGeometry.Scheme.Modules.tensorSections_zero_left
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
attribute [local instance] MvPolynomial.gradedAlgebra
namespace W2FINSketch

Lean source · full declaration

def tensorPowIso {X : Scheme.{u}} {L L' : X.Modules} (e : L ≅ L') :
    (b : ℕ) → (L.tensorPow b ≅ L'.tensorPow b)
  | 0 => Iso.refl _
  | b + 1 => tensorPowIso e b ⊗ᵢ e

theorem

exists_finiteBySections_tensorPow_of_forall_geometricFibre

L84 ↗

AlgebraicGeometry.Scheme.Modules.exists_finiteBySections_tensorPow_of_forall_geometricFibre