NYLL
Module

TensorLinearDualComplex.lean

Nyll.EtaleFundamentalGroups.Purity.TensorLinearDualComplex
4 declarations indexed from sourceView source ↗

Module documentation

Tensor coefficients and linear-dual complexes

The tensor--Hom correspondence is linear and natural in the variable complex. Consequently applying linear Hom from a coefficient module to the dual complex agrees with dualizing the complex after tensoring with that coefficient module. If the original terms are flat and the dual values are injective, the dual terms are injective.

Imports6
Imported by3

Declarations

def

tensorLinearDualHomEquiv

L37 ↗
EtaleFundamentalGroups.Purity.tensorLinearDualHomEquiv
Documentation

The tensor--Hom correspondence with bundled module morphisms, including its linear structure.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u v
open CategoryTheory Opposite MonoidalCategory
open scoped TensorProduct
variable {R : Type u} [CommRing R]
Lean source · full declaration
def tensorLinearDualHomEquiv (M N E : ModuleCat.{u} R) :
    (M ⟶ ModuleCat.of R (N ⟶ E)) ≃ₗ[R] (M ⊗ N ⟶ E) where
  toFun f := ModuleCat.ofHom (TensorProduct.lift f.hom₂)
  invFun g := ModuleCat.ofHom₂ (TensorProduct.curry g.hom)
  left_inv f := by
    ext m n
    rfl
  right_inv g := by
    ext m n
    rfl
  map_add' f g := by
    ext m n
    rfl
  map_smul' a f := by
    ext m n
    rfl
def

tensorLinearDualHomIso

L55 ↗
EtaleFundamentalGroups.Purity.tensorLinearDualHomIso
Documentation

Naturality of tensor--Hom in the contravariant module argument.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u v
open CategoryTheory Opposite MonoidalCategory
open scoped TensorProduct
variable {R : Type u} [CommRing R]
Lean source · statement
def tensorLinearDualHomIso (M E : ModuleCat.{u} R) :
    (linearYoneda R (ModuleCat.{u} R)).obj E ⋙
        (linearCoyoneda R (ModuleCat.{u} R)).obj (op M) ≅
      (tensorLeft M).op ⋙ (linearYoneda R (ModuleCat.{u} R)).obj E
def

tensorLinearDualComplexIso

L73 ↗
EtaleFundamentalGroups.Purity.tensorLinearDualComplexIso
Documentation

Hom from a module into a reversed dual complex is the reversed dual of the complex with tensor coefficients.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u v
open CategoryTheory Opposite MonoidalCategory
open scoped TensorProduct
variable {R : Type u} [CommRing R]
Lean source · statement
def tensorLinearDualComplexIso
    (M E : ModuleCat.{u} R) {ι : Type v} {c : ComplexShape ι}
    (K : HomologicalComplex (ModuleCat.{u} R) c) :
    (((linearCoyoneda R (ModuleCat.{u} R)).obj (op M)).mapHomologicalComplex
        c.symm).obj (linearDualComplex E K) ≅
      linearDualComplex E ((tensorLeft M).mapHomologicalComplex c |>.obj K)
theorem

injective_linearDualComplex_X

L82 ↗
EtaleFundamentalGroups.Purity.injective_linearDualComplex_X
Documentation

Each term of the injective-valued dual of a flat complex is injective.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u v
open CategoryTheory Opposite MonoidalCategory
open scoped TensorProduct
variable {R : Type u} [CommRing R]
Lean source · statement
theorem injective_linearDualComplex_X
    (E : ModuleCat.{u} R) [Module.Injective R E]
    {ι : Type v} {c : ComplexShape ι}
    (K : HomologicalComplex (ModuleCat.{u} R) c) (j : ι)
    [Module.Flat R (K.X j)] :
    Module.Injective R ((linearDualComplex E K).X j)

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