NYLL
Module

Scheme_Modules_IsInvertible_isIso_ev_app_tensorUnit.lean

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

Module documentation

Evaluation against the dual of an invertible module

For an invertible module, evaluation against its dual is an isomorphism when applied to the unit module.

Imports6
Imported by10

Declarations

def

tensorLeftEquivalence

L57 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isIso_ev_app_tensorUnit.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_isIso_ev_app_tensorUnit
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_isIso_ev_app_tensorUnit.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_isIso_ev_app_tensorUnit
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_isIso_ev_app_tensorUnit.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_isIso_ev_app_tensorUnit
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_isIso_ev_app_tensorUnit.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_isIso_ev_app_tensorUnit
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_isIso_ev_app_tensorUnit.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_isIso_ev_app_tensorUnit
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_isIso_ev_app_tensorUnit.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_isIso_ev_app_tensorUnit
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_isIso_ev_app_tensorUnit.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_isIso_ev_app_tensorUnit
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_isIso_ev_app_tensorUnit.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_isIso_ev_app_tensorUnit
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

isIso_ev_app_tensorUnit

L164 ↗
AlgebraicGeometry.Scheme.Modules.IsInvertible.isIso_ev_app_tensorUnit
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isIso_ev_app_tensorUnit
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_isIso_ev_app_tensorUnit.AlgebraicGeometry in
with_weak_namespace Scheme_Modules_IsInvertible_isIso_ev_app_tensorUnit
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible.isIso_ev_app_tensorUnit
    {Y : Scheme.{u}} {X : Y.Modules} (hX : Scheme.Modules.IsInvertible X) :
    IsIso ((ihom.ev X).app (𝟙_ Y.Modules))

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