Module

InjectiveLinearDualHomology.lean

Nyll.EtaleFundamentalGroups.Purity.InjectiveLinearDualHomology

4 declarations indexed from sourceView source ↗

Module documentation

Linear duals with injective values and homology

The contravariant linear Hom functor with injective values is exact. This is obtained from preadditive Yoneda exactness by the forgetful functor, which reflects finite limits and colimits. Applying the exact functor to an opposite complex identifies its homology with the linear dual of the original homology, without changing the scalar ring.

Imports11

Mathlib.Algebra.Category.ModuleCat.Abelian
Mathlib.Algebra.Category.ModuleCat.Colimits
Mathlib.Algebra.Category.ModuleCat.Injective
Mathlib.Algebra.Category.ModuleCat.Limits
Mathlib.Algebra.Homology.Additive
Mathlib.Algebra.Homology.Opposite
Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Mathlib.CategoryTheory.Abelian.Injective.Basic
Mathlib.CategoryTheory.Linear.Yoneda
Mathlib.CategoryTheory.Limits.Preserves.Finite

Imported by4

theorem

linearYoneda_preservesHomology_of_injective

L41 ↗

EtaleFundamentalGroups.Purity.linearYoneda_preservesHomology_of_injective

Documentation

Linear Yoneda with injective values preserves homology. The property is supplied explicitly instead of adding a competing global instance.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u v
open CategoryTheory Limits Opposite
variable {R : Type u} [CommRing R]

Lean source · statement

theorem linearYoneda_preservesHomology_of_injective
    (E : ModuleCat.{u} R) [Module.Injective R E] :
    ((linearYoneda R (ModuleCat.{u} R)).obj E).PreservesHomology

def

injectiveLinearDualShortComplexHomologyIso

L65 ↗

EtaleFundamentalGroups.Purity.injectiveLinearDualShortComplexHomologyIso

Documentation

The homology of a reversed linear-dual short complex is the linear dual of the original homology when the values are injective.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u v
open CategoryTheory Limits Opposite
variable {R : Type u} [CommRing R]

Lean source · statement

def injectiveLinearDualShortComplexHomologyIso
    (E : ModuleCat.{u} R) [Module.Injective R E]
    (S : ShortComplex (ModuleCat.{u} R)) :
    (S.op.map ((linearYoneda R (ModuleCat.{u} R)).obj E)).homology ≅
      ModuleCat.of R (S.homology →ₗ[R] E)

def

linearDualComplex

L78 ↗

EtaleFundamentalGroups.Purity.linearDualComplex

Documentation

The complex obtained by reversing arrows and applying the linear Hom functor with values in the given module.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u v
open CategoryTheory Limits Opposite
variable {R : Type u} [CommRing R]

Lean source · statement

def linearDualComplex
    (E : ModuleCat.{u} R) {ι : Type v} {c : ComplexShape ι}
    (K : HomologicalComplex (ModuleCat.{u} R) c) :
    HomologicalComplex (ModuleCat.{u} R) c.symm

def

injectiveLinearDualComplexHomologyIso

L86 ↗

EtaleFundamentalGroups.Purity.injectiveLinearDualComplexHomologyIso

Documentation

Homology commutes with the linear dual into an injective module, with the complex shape reversed.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u v
open CategoryTheory Limits Opposite
variable {R : Type u} [CommRing R]

Lean source · statement

def injectiveLinearDualComplexHomologyIso
    (E : ModuleCat.{u} R) [Module.Injective R E]
    {ι : Type v} {c : ComplexShape ι}
    (K : HomologicalComplex (ModuleCat.{u} R) c) (j : ι) :
    (linearDualComplex E K).homology j ≅ ModuleCat.of R (K.homology j →ₗ[R] E)

Module documentation

Linear duals with injective values and homology

Declarations

linearYoneda_preservesHomology_of_injective

injectiveLinearDualShortComplexHomologyIso

linearDualComplex

injectiveLinearDualComplexHomologyIso