Module

Scheme_Modules_nonempty_pullback_tensorPow_iso.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_pullback_tensorPow_iso

2 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules nonempty pullback tensor Pow iso

Imports3

Imported by8

def

pullbackTensorPowIso

L45 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_tensorPow_iso.AlgebraicGeometry.Scheme.Modules.pullbackTensorPowIso

Documentation

The isomorphism identifying the pullback of a tensor power with the tensor power of the pullback.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_tensorPow_iso
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open scoped _root_.AlgebraicGeometry _root_.AlgebraicGeometry.Scheme
  _root_.AlgebraicGeometry.Scheme.Modules in

Lean source · full declaration

def AlgebraicGeometry.Scheme.Modules.pullbackTensorPowIso
    {X Y : Scheme.{u}} (f : X ⟶ Y) (L : Y.Modules) :
    ∀ n : ℕ, (Scheme.Modules.pullback f).obj (L.tensorPow n) ≅ ((Scheme.Modules.pullback f).obj
      L).tensorPow n
  | 0 => Scheme.Modules.pullbackTensorUnitObjIso f
  | n + 1 => Scheme.Modules.pullbackTensorObjIso f (L.tensorPow n) L ≪≫
      whiskerRightIso (AlgebraicGeometry.Scheme.Modules.pullbackTensorPowIso f L n) _

theorem

nonempty_pullback_tensorPow_iso

L53 ↗

AlgebraicGeometry.Scheme.Modules.nonempty_pullback_tensorPow_iso

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_tensorPow_iso
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.nonempty_pullback_tensorPow_iso
    {X Y : Scheme.{u}} (f : X ⟶ Y) (L : Y.Modules) (n : ℕ) :
    Nonempty ((Scheme.Modules.pullback f).obj (L.tensorPow n) ≅ ((Scheme.Modules.pullback f).obj
      L).tensorPow n)

Module documentation

Scheme Modules nonempty pullback tensor Pow iso

Declarations

pullbackTensorPowIso

nonempty_pullback_tensorPow_iso