LeanPool.BrauerGroupNew.Examples.ShortComplex.LeftHomologyMapData

Imported Lean Pool material for LeanPool.BrauerGroupNew.Examples.ShortComplex.LeftHomologyMapData.

@[reducible, inline]

abbrev φK (R : Type u) [CommRing R] (S₁ : CategoryTheory.ShortComplex (ModuleCat R)) (S₂ : CategoryTheory.ShortComplex (ModuleCat R)) (f : S₁ ⟶ S₂) : ↥(ModuleCat.Hom.hom S₁.g).ker →ₗ[R] ↥(ModuleCat.Hom.hom S₂.g).ker

The map on explicit cycle modules induced by a morphism of short complexes.

Equations

• φK R S₁ S₂ f = (ModuleCat.Hom.hom f.τ₂).restrict ⋯

theorem φK_moduleCatToCycles (R : Type u) [CommRing R] (S₁ : CategoryTheory.ShortComplex (ModuleCat R)) (S₂ : CategoryTheory.ShortComplex (ModuleCat R)) (f : S₁ ⟶ S₂) (x : ↑S₁.X₁) : (φK R S₁ S₂ f) (S₁.moduleCatToCycles x) = S₂.moduleCatToCycles ((CategoryTheory.ConcreteCategory.hom f.τ₁) x)

The map on cycles carries boundaries to boundaries.

theorem φK_maps_moduleCatToCycles_range (R : Type u) [CommRing R] (S₁ : CategoryTheory.ShortComplex (ModuleCat R)) (S₂ : CategoryTheory.ShortComplex (ModuleCat R)) (f : S₁ ⟶ S₂) : S₁.moduleCatToCycles.range ≤ Submodule.comap (φK R S₁ S₂ f) S₂.moduleCatToCycles.range

The map on cycles descends to the quotient by boundaries.

@[reducible, inline]

abbrev φH (R : Type u) [CommRing R] (S₁ : CategoryTheory.ShortComplex (ModuleCat R)) (S₂ : CategoryTheory.ShortComplex (ModuleCat R)) (f : S₁ ⟶ S₂) : ModuleCat.of R (↥(ModuleCat.Hom.hom S₁.g).ker ⧸ S₁.moduleCatToCycles.range) ⟶ ModuleCat.of R (↥(ModuleCat.Hom.hom S₂.g).ker ⧸ S₂.moduleCatToCycles.range)

The induced map on explicit module-category left homology quotients.

Equations

• φH R S₁ S₂ f = ModuleCat.ofHom (S₁.moduleCatToCycles.range.mapQ S₂.moduleCatToCycles.range (φK R S₁ S₂ f) ⋯)

def LeftHomologyMapData.ofModuleCat (R : Type u) [CommRing R] (S₁ : CategoryTheory.ShortComplex (ModuleCat R)) (S₂ : CategoryTheory.ShortComplex (ModuleCat R)) (f : S₁ ⟶ S₂) : CategoryTheory.ShortComplex.LeftHomologyMapData f S₁.moduleCatLeftHomologyData S₂.moduleCatLeftHomologyData

The explicit left homology map data for a morphism of short complexes of modules.

Equations

• LeftHomologyMapData.ofModuleCat R S₁ S₂ f = { φK := ModuleCat.ofHom (φK R S₁ S₂ f), φH := φH R S₁ S₂ f, commi := ⋯, commf' := ⋯, commπ := ⋯ }

@[simp]

theorem LeftHomologyMapData.ofModuleCat_φK (R : Type u) [CommRing R] (S₁ : CategoryTheory.ShortComplex (ModuleCat R)) (S₂ : CategoryTheory.ShortComplex (ModuleCat R)) (f : S₁ ⟶ S₂) : (ofModuleCat R S₁ S₂ f).φK = ModuleCat.ofHom (φK R S₁ S₂ f)

@[simp]

theorem LeftHomologyMapData.ofModuleCat_φH (R : Type u) [CommRing R] (S₁ : CategoryTheory.ShortComplex (ModuleCat R)) (S₂ : CategoryTheory.ShortComplex (ModuleCat R)) (f : S₁ ⟶ S₂) : (ofModuleCat R S₁ S₂ f).φH = φH R S₁ S₂ f

theorem ShortComplex.IsQuasiIsoAt_iff_moduleCat (R : Type u) [CommRing R] (S₁ : CategoryTheory.ShortComplex (ModuleCat R)) (S₂ : CategoryTheory.ShortComplex (ModuleCat R)) (f : S₁ ⟶ S₂) : CategoryTheory.ShortComplex.QuasiIso f ↔ (∀ (a : ↑S₁.X₂), (ModuleCat.Hom.hom S₁.g) a = 0 → ∀ (x : ↑S₂.X₁), (CategoryTheory.ConcreteCategory.hom S₂.f) x = (ModuleCat.Hom.hom f.τ₂) a → ∃ (y : ↑S₁.X₁), (CategoryTheory.ConcreteCategory.hom S₁.f) y = a) ∧ ∀ (a : ↑S₂.X₂), (ModuleCat.Hom.hom S₂.g) a = 0 → ∃ (a_1 : ↑S₁.X₂), (ModuleCat.Hom.hom S₁.g) a_1 = 0 ∧ ∃ (y : ↑S₂.X₁), (CategoryTheory.ConcreteCategory.hom S₂.f) y = (ModuleCat.Hom.hom f.τ₂) a_1 - a

A concrete quotient criterion for quasi-isomorphisms of short complexes of modules.