NYLL
Module

Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff
9 declarations indexed from sourceView source ↗

Module documentation

Vanishing of a transposed section after pullback

For an invertible source module, the section transposed from a module morphism vanishes after pullback exactly when the pulled-back morphism vanishes.

Imports6
Imported by3

Declarations

def

tensorLeftEquivalence

L57 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff.AlgebraicGeometry.Scheme.Modules.CoevAux.tensorLeftEquivalence
Documentation

The equivalence given by tensoring on the left with an invertible module.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff
section E6Coev
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace CoevAux
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
def tensorLeftEquivalence {Z Z' : Y.Modules} (i : Z' ⊗ Z ≅ 𝟙_ Y.Modules) (j : Z ⊗ Z' ≅ 𝟙_
    Y.Modules) :
    Y.Modules ≌ Y.Modules
def

tensorRightEquivalence

L67 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff.AlgebraicGeometry.Scheme.Modules.CoevAux.tensorRightEquivalence
Documentation

The equivalence given by tensoring on the right with an invertible module.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff
section E6Coev
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace CoevAux
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
def tensorRightEquivalence {Z Z' : Y.Modules} (i : Z' ⊗ Z ≅ 𝟙_ Y.Modules) (j : Z ⊗ Z' ≅ 𝟙_
    Y.Modules) :
    Y.Modules ≌ Y.Modules
theorem

isEquivalence_tensorLeft

L76 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff.AlgebraicGeometry.Scheme.Modules.CoevAux.isEquivalence_tensorLeft
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff
section E6Coev
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace CoevAux
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem isEquivalence_tensorLeft {Z : Y.Modules} (hZ : Scheme.Modules.IsInvertible Z) :
    (tensorLeft Z).IsEquivalence
theorem

isEquivalence_tensorRight

L80 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff.AlgebraicGeometry.Scheme.Modules.CoevAux.isEquivalence_tensorRight
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff
section E6Coev
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace CoevAux
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem isEquivalence_tensorRight {Z : Y.Modules} (hZ : Scheme.Modules.IsInvertible Z) :
    (tensorRight Z).IsEquivalence
theorem

isIso_ev_app

L84 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff.AlgebraicGeometry.Scheme.Modules.CoevAux.isIso_ev_app
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff
section E6Coev
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace CoevAux
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem isIso_ev_app (X : Y.Modules) (hX : Scheme.Modules.IsInvertible X) (N : Y.Modules) :
    IsIso ((ihom.ev X).app N)
theorem

whiskerRight_eq_zero_iff

L94 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff.AlgebraicGeometry.Scheme.Modules.CoevAux.whiskerRight_eq_zero_iff
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff
section E6Coev
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace CoevAux
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem whiskerRight_eq_zero_iff {L M Z : Y.Modules} (hZ : Scheme.Modules.IsInvertible Z) (f : L
    ⟶ M) :
    f ▷ Z = 0 ↔ f = 0
theorem

transposeSection_eq_zero_iff'

L106 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff.AlgebraicGeometry.Scheme.Modules.CoevAux.transposeSection_eq_zero_iff'
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff
section E6Coev
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace CoevAux
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem transposeSection_eq_zero_iff' {X M : Y.Modules} (hX : Scheme.Modules.IsInvertible X) (φ
    : X ⟶ M)
    (s : 𝟙_ Y.Modules ⟶ M ⊗ Scheme.Modules.dual X)
    (hs : (ihom.ev X).app (𝟙_ Y.Modules) ≫ s = φ ▷ Scheme.Modules.dual X) :
    s = 0 ↔ φ = 0
theorem

pullbackSection_transposeSection_eq_zero_iff'

L115 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff.AlgebraicGeometry.Scheme.Modules.CoevAux.pullbackSection_transposeSection_eq_zero_iff'
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff
section E6Coev
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace CoevAux
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem pullbackSection_transposeSection_eq_zero_iff' {Y' : Scheme.{u}} (g : Y' ⟶ Y) {X M :
    Y.Modules}
    (hX : Scheme.Modules.IsInvertible X) (φ : X ⟶ M)
    (s : 𝟙_ Y.Modules ⟶ M ⊗ Scheme.Modules.dual X)
    (hs : (ihom.ev X).app (𝟙_ Y.Modules) ≫ s = φ ▷ Scheme.Modules.dual X) :
    Scheme.Modules.pullbackSection g s = 0 ↔ (Scheme.Modules.pullback g).map φ = 0
theorem

pullbackSection_transposeSection_eq_zero_iff

L166 ↗
AlgebraicGeometry.Scheme.Modules.IsInvertible.pullbackSection_transposeSection_eq_zero_iff
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff
section E6Coev
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
with_weak_namespace _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open CategoryTheory CategoryTheory.Limits _root_.CategoryTheory.MonoidalCategory
    _root_.AlgebraicGeometry
    Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff.AlgebraicGeometry in
with_weak_namespace Scheme_Modules_IsInvertible_pullbackSection_transposeSection_eq_zero_iff
open AlgebraicGeometry.Scheme.Modules.CoevAux in
with_weak_namespace _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible
Lean source · statement
theorem pullbackSection_transposeSection_eq_zero_iff
    {Y Y' : Scheme.{u}} (g : Y' ⟶ Y) {X M : Y.Modules} (hX : Scheme.Modules.IsInvertible X) (φ :
        X ⟶ M)
    (s : 𝟙_ Y.Modules ⟶ M ⊗ Scheme.Modules.dual X)
    (hs : (ihom.ev X).app (𝟙_ Y.Modules) ≫ s = φ ▷ Scheme.Modules.dual X) :
    Scheme.Modules.pullbackSection g s = 0 ↔ (Scheme.Modules.pullback g).map φ = 0

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