Documentation

TauCeti.Algebra.Homology.ModuleCat.Biprod

Biproducts of complexes of modules #

A short complex K ⟶ L₁ ⊞ L₂ ⟶ N of homological complexes of modules whose maps are biprod.lift a₁ a₂ and biprod.desc b₁ b₂ is short exact as soon as, in each degree and under given identifications of the terms with modules, the linear maps (a₁, a₂) : K → L₁ × L₂ and b₁ + b₂ : L₁ × L₂ → N form a short exact sequence of modules (HomologicalComplex.moduleCat_shortExact_biprod). Mayer–Vietoris sequences have this shape.

The comparison uses ModuleCat.inl_comp_biprodIsoProd_hom and ModuleCat.inr_comp_biprodIsoProd_hom from TauCeti.Algebra.Category.ModuleCat.Biproducts: under Mathlib's identification ModuleCat.biprodIsoProd of the biproduct of two modules with their product, the biproduct inclusions are LinearMap.inl and LinearMap.inr. Along the same identification, bases of K.X i and L.X i give the basis HomologicalComplex.biprodXBasis of (K ⊞ L).X i, made of their images under the two biproduct inclusions; this is how a direct sum of based complexes is based.

On elements, biprod.lift and biprod.desc act componentwise (HomologicalComplex.biprod_desc_f_apply, HomologicalComplex.biprod_lift_f_apply), which is how elements of the middle term of a Mayer–Vietoris sequence are handled.

References #

source
theorem HomologicalComplex.moduleCat_shortExact_biprod {R : Type u} [Ring R] {ι : Type u_1} {c : ComplexShape ι} {K L₁ L₂ N : HomologicalComplex (ModuleCat R) c} {K' L₁' L₂' N' : ι → Type v} [(i : ι) → AddCommGroup (K' i)] [(i : ι) → Module R (K' i)] [(i : ι) → AddCommGroup (L₁' i)] [(i : ι) → Module R (L₁' i)] [(i : ι) → AddCommGroup (L₂' i)] [(i : ι) → Module R (L₂' i)] [(i : ι) → AddCommGroup (N' i)] [(i : ι) → Module R (N' i)] {a₁ : K ⟶ L₁} {a₂ : K ⟶ L₂} {b₁ : L₁ ⟶ N} {b₂ : L₂ ⟶ N} (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift a₁ a₂) (CategoryTheory.Limits.biprod.desc b₁ b₂) = 0) (eK : (i : ι) → K.X i ≅ ↧(K' i)) (eL₁ : (i : ι) → L₁.X i ≅ ↧(L₁' i)) (eL₂ : (i : ι) → L₂.X i ≅ ↧(L₂' i)) (eN : (i : ι) → N.X i ≅ ↧(N' i)) (a₁' : (i : ι) → K' i →ₗ[R] L₁' i) (a₂' : (i : ι) → K' i →ₗ[R] L₂' i) (b₁' : (i : ι) → L₁' i →ₗ[R] N' i) (b₂' : (i : ι) → L₂' i →ₗ[R] N' i) (ha₁ : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a₁.f i) (eL₁ i).hom = CategoryTheory.CategoryStruct.comp (eK i).hom (ModuleCat.ofHom (a₁' i))) (ha₂ : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a₂.f i) (eL₂ i).hom = CategoryTheory.CategoryStruct.comp (eK i).hom (ModuleCat.ofHom (a₂' i))) (hb₁ : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (b₁.f i) (eN i).hom = CategoryTheory.CategoryStruct.comp (eL₁ i).hom (ModuleCat.ofHom (b₁' i))) (hb₂ : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (b₂.f i) (eN i).hom = CategoryTheory.CategoryStruct.comp (eL₂ i).hom (ModuleCat.ofHom (b₂' i))) (hexact : ∀ (i : ι), Function.Exact ⇑((a₁' i).prod (a₂' i)) ⇑((b₁' i).coprod (b₂' i))) (hinj : ∀ (i : ι), Function.Injective ⇑((a₁' i).prod (a₂' i))) (hsurj : ∀ (i : ι), Function.Surjective ⇑((b₁' i).coprod (b₂' i))) :
{ X₁ := K, X₂ := L₁ ⊞ L₂, X₃ := N, f := CategoryTheory.Limits.biprod.lift a₁ a₂, g := CategoryTheory.Limits.biprod.desc b₁ b₂, zero := w }.ShortExact

A short complex K ⟶ L₁ ⊞ L₂ ⟶ N of complexes of modules, with maps biprod.lift a₁ a₂ and biprod.desc b₁ b₂, is short exact when, in each degree and under identifications of the terms with modules K' i, L₁' i, L₂' i, N' i carrying the components to linear maps a₁' i, a₂' i, b₁' i, b₂' i, the pair map (a₁' i).prod (a₂' i) is injective, the sum map (b₁' i).coprod (b₂' i) is surjective, and the two are exact.

source
noncomputable def HomologicalComplex.biprodXBasis {R : Type u} [Ring R] {ι : Type u_1} {c : ComplexShape ι} {K L : HomologicalComplex (ModuleCat R) c} {i : ι} {κ : Type u_2} {σ : Type u_3} (b : Module.Basis κ R ↑(K.X i)) (b' : Module.Basis σ R ↑(L.X i)) :
Module.Basis (κ ⊕ σ) R ↑((K ⊞ L).X i)

The basis of the term (K ⊞ L).X i of a biproduct of complexes of modules made of the images of a basis b of K.X i under biprod.inl, followed by the images of a basis b' of L.X i under biprod.inr.

Instances For
    source
    theorem HomologicalComplex.inl_f_comp_biprodXIso_trans_biprodIsoProd_hom {R : Type u} [Ring R] {ι : Type u_1} {c : ComplexShape ι} (K L : HomologicalComplex (ModuleCat R) c) (i : ι) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) (K.biprodXIso L i ≪≫ (K.X i).biprodIsoProd (L.X i)).hom = ModuleCat.ofHom (LinearMap.inl R ↑(K.1 i) ↑(L.X i))

    Under the identification biprodXIso K L i ≪≫ ModuleCat.biprodIsoProd _ _ of (K ⊞ L).X i with the product module K.X i × L.X i, the first biproduct inclusion is LinearMap.inl.

    source
    theorem HomologicalComplex.inr_f_comp_biprodXIso_trans_biprodIsoProd_hom {R : Type u} [Ring R] {ι : Type u_1} {c : ComplexShape ι} (K L : HomologicalComplex (ModuleCat R) c) (i : ι) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) (K.biprodXIso L i ≪≫ (K.X i).biprodIsoProd (L.X i)).hom = ModuleCat.ofHom (LinearMap.inr R ↑(K.X i) ↑(L.1 i))

    Under the identification biprodXIso K L i ≪≫ ModuleCat.biprodIsoProd _ _ of (K ⊞ L).X i with the product module K.X i × L.X i, the second biproduct inclusion is LinearMap.inr.

    source
    @[simp]
    theorem HomologicalComplex.biprodXBasis_inl {R : Type u} [Ring R] {ι : Type u_1} {c : ComplexShape ι} {K L : HomologicalComplex (ModuleCat R) c} {i : ι} {κ : Type u_2} {σ : Type u_3} (b : Module.Basis κ R ↑(K.X i)) (b' : Module.Basis σ R ↑(L.X i)) (k : κ) :
    (biprodXBasis b b') (Sum.inl k) = (ModuleCat.Hom.hom (CategoryTheory.Limits.biprod.inl.f i)) (b k)
    source
    @[simp]
    theorem HomologicalComplex.biprodXBasis_inr {R : Type u} [Ring R] {ι : Type u_1} {c : ComplexShape ι} {K L : HomologicalComplex (ModuleCat R) c} {i : ι} {κ : Type u_2} {σ : Type u_3} (b : Module.Basis κ R ↑(K.X i)) (b' : Module.Basis σ R ↑(L.X i)) (k : σ) :
    (biprodXBasis b b') (Sum.inr k) = (ModuleCat.Hom.hom (CategoryTheory.Limits.biprod.inr.f i)) (b' k)

    Elements of biproducts of complexes of modules #

    source
    theorem HomologicalComplex.biprod_desc_f_apply {R : Type u} [Ring R] {ι : Type u_1} {c : ComplexShape ι} {K K₁ K₂ : HomologicalComplex (ModuleCat R) c} (φ₁ : K₁ ⟶ K) (φ₂ : K₂ ⟶ K) (i : ι) (x : ↑((K₁ ⊞ K₂).X i)) :
    (ModuleCat.Hom.hom ((CategoryTheory.Limits.biprod.desc φ₁ φ₂).f i)) x = (ModuleCat.Hom.hom (φ₁.f i)) ((ModuleCat.Hom.hom (CategoryTheory.Limits.biprod.fst.f i)) x) + (ModuleCat.Hom.hom (φ₂.f i)) ((ModuleCat.Hom.hom (CategoryTheory.Limits.biprod.snd.f i)) x)

    biprod.desc φ₁ φ₂ sends an element x of a term of K₁ ⊞ K₂ to the sum of the images of its two components.

    source
    theorem HomologicalComplex.biprod_lift_f_apply {R : Type u} [Ring R] {ι : Type u_1} {c : ComplexShape ι} {K K₁ K₂ : HomologicalComplex (ModuleCat R) c} (ψ₁ : K ⟶ K₁) (ψ₂ : K ⟶ K₂) (i : ι) (x : ↑(K.X i)) :
    (ModuleCat.Hom.hom ((CategoryTheory.Limits.biprod.lift ψ₁ ψ₂).f i)) x = (ModuleCat.Hom.hom (CategoryTheory.Limits.biprod.inl.f i)) ((ModuleCat.Hom.hom (ψ₁.f i)) x) + (ModuleCat.Hom.hom (CategoryTheory.Limits.biprod.inr.f i)) ((ModuleCat.Hom.hom (ψ₂.f i)) x)

    biprod.lift ψ₁ ψ₂ sends an element x of a term of K to the sum of the inclusions of its two images.