Module

IsAlgEquivZero_tensorPow.lean

Nyll.JacobianVarieties.Picard.IsAlgEquivZero_tensorPow

3 declarations indexed from sourceView source ↗

Module documentation

Tensor powers of an algebraically trivial invertible module remain algebraically trivial.

Imports3

Imported by2

theorem

unit

L45 ↗

JacobianVarieties.Picard.Proofs.S_AlgebraicGeometry_RelPicard_IsAlgEquivZero_tensorPow.AezTensorPow.unit

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.S_AlgebraicGeometry_RelPicard_IsAlgEquivZero_tensorPow
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
namespace AezTensorPow
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard

Lean source · statement

theorem unit {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k)) :
    IsAlgEquivZero a (𝟙_ A.Modules)

theorem

main

L55 ↗

JacobianVarieties.Picard.Proofs.S_AlgebraicGeometry_RelPicard_IsAlgEquivZero_tensorPow.AezTensorPow.main

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.S_AlgebraicGeometry_RelPicard_IsAlgEquivZero_tensorPow
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
namespace AezTensorPow
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard

Lean source · statement

theorem main {k : Type u} [Field k] {A : Scheme.{u}} {a : A ⟶ Spec (CommRingCat.of k)}
    {L : A.Modules}
    (hL : IsAlgEquivZero a L) (n : ℕ) : IsAlgEquivZero a (L.tensorPow n)

theorem

tensorPow

L68 ↗

AlgebraicGeometry.RelPicard.IsAlgEquivZero.tensorPow

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.S_AlgebraicGeometry_RelPicard_IsAlgEquivZero_tensorPow
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits _root_.CategoryTheory.MonoidalCategory in
open AlgebraicGeometry AlgebraicGeometry.RelPicard in

Lean source · statement

theorem _root_.AlgebraicGeometry.RelPicard.IsAlgEquivZero.tensorPow
    {k : Type u} [Field k] {A : Scheme.{u}} {a : A ⟶ Spec (CommRingCat.of k)} {L : A.Modules}
    (hL : IsAlgEquivZero a L) (n : ℕ) : IsAlgEquivZero a (L.tensorPow n)

Module documentation

Declarations

unit

main

tensorPow