Documentation

TauCeti.Algebra.Homology.ModuleCat.Minimal

Minimal complexes of modules #

A complex over a commutative ring is minimal if every differential takes values in the Jacobson radical times its target. Over a local ring this is the usual maximal-ideal criterion for minimal free resolutions. Finiteness and projectivity of the terms are separate hypotheses, not part of minimality.

A self-map of a minimal complex of finite modules that is homotopic to the identity is invertible. Consequently a homotopy equivalence between two such complexes is already an isomorphism of complexes. No boundedness, freeness, or Noetherian hypothesis is needed. This rigidity allows properties of the actual terms and differentials, such as periodic tails, to be recovered from minimal representatives in the homotopy category.

References #

source
def HomologicalComplex.IsMinimal {R : Type u} [CommRing R] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat R) c) :
Prop

A complex of modules is minimal if each differential has image in the Jacobson radical of the ring times its target module.

Instances For
    source
    theorem HomologicalComplex.isMinimal_iff {R : Type u} [CommRing R] {ι : Type u_1} {c : ComplexShape ι} {K : HomologicalComplex (ModuleCat R) c} :
    K.IsMinimal ↔ ∀ (i j : ι), (ModuleCat.Hom.hom (K.d i j)).range ≤ Ring.jacobson R • ⊤

    The image criterion characterizing minimal complexes.

    source
    theorem HomologicalComplex.isMinimal_iff_forall_rel {R : Type u} [CommRing R] {ι : Type u_1} {c : ComplexShape ι} {K : HomologicalComplex (ModuleCat R) c} :
    K.IsMinimal ↔ ∀ (i j : ι), c.Rel i j → (ModuleCat.Hom.hom (K.d i j)).range ≤ Ring.jacobson R • ⊤

    Minimality can be checked just on the differentials allowed by the complex shape.

    source
    theorem HomologicalComplex.IsMinimal.d_apply_mem {R : Type u} [CommRing R] {ι : Type u_1} {c : ComplexShape ι} {K : HomologicalComplex (ModuleCat R) c} (hK : K.IsMinimal) (i j : ι) (x : ↑(K.X i)) :
    (ModuleCat.Hom.hom (K.d i j)) x ∈ Ring.jacobson R • ⊤

    Every value of a differential in a minimal complex lies in the radical times its target.

    source
    theorem HomologicalComplex.isMinimal_iff_range_le_maximalIdeal_smul {R : Type u} [CommRing R] {ι : Type u_1} {c : ComplexShape ι} {K : HomologicalComplex (ModuleCat R) c} [IsLocalRing R] :
    K.IsMinimal ↔ ∀ (i j : ι), (ModuleCat.Hom.hom (K.d i j)).range ≤ IsLocalRing.maximalIdeal R • ⊤

    Over a local ring, minimality is the usual maximal-ideal image criterion.

    source
    theorem HomologicalComplex.IsMinimal.of_iso {R : Type u} [CommRing R] {ι : Type u_1} {c : ComplexShape ι} {K L : HomologicalComplex (ModuleCat R) c} (hK : K.IsMinimal) (e : K ≅ L) :
    L.IsMinimal

    Minimality is preserved by isomorphisms of complexes.

    source
    theorem HomologicalComplex.IsMinimal.sub_mem_of_homotopy {R : Type u} [CommRing R] {ι : Type u_1} {c : ComplexShape ι} {K L : HomologicalComplex (ModuleCat R) c} (hK : K.IsMinimal) (hL : L.IsMinimal) {f g : K ⟶ L} (h : Homotopy f g) (i : ι) (x : ↑(K.X i)) :
    (ModuleCat.Hom.hom (f.f i)) x - (ModuleCat.Hom.hom (g.f i)) x ∈ Ring.jacobson R • ⊤

    Homotopic maps between minimal complexes agree modulo the radical in every degree.

    source
    theorem HomologicalComplex.IsMinimal.isIso_of_homotopy_id {R : Type u} [CommRing R] {ι : Type u_1} {c : ComplexShape ι} {K : HomologicalComplex (ModuleCat R) c} (hK : K.IsMinimal) [∀ (i : ι), Module.Finite R ↑(K.X i)] {f : K ⟶ K} (h : Homotopy f (CategoryTheory.CategoryStruct.id K)) :
    CategoryTheory.IsIso f

    A self-map homotopic to the identity on a minimal complex of finite modules is an isomorphism.

    source
    theorem HomologicalComplex.IsMinimal.isIso_hom_of_homotopyEquiv {R : Type u} [CommRing R] {ι : Type u_1} {c : ComplexShape ι} {K L : HomologicalComplex (ModuleCat R) c} (hK : K.IsMinimal) (hL : L.IsMinimal) [∀ (i : ι), Module.Finite R ↑(K.X i)] [∀ (i : ι), Module.Finite R ↑(L.X i)] (e : HomotopyEquiv K L) :
    CategoryTheory.IsIso e.hom

    A homotopy equivalence between minimal complexes of finite modules is already an isomorphism on its forward chain map.

    source
    theorem ChainComplex.isMinimal_iff_range_d_succ_le {R : Type u} [CommRing R] {K : ChainComplex (ModuleCat R) ℕ} :
    HomologicalComplex.IsMinimal K ↔ ∀ (n : ℕ), (ModuleCat.Hom.hom (K.d (n + 1) n)).range ≤ Ring.jacobson R • ⊤

    A natural-number-indexed chain complex is minimal exactly when each successive differential has image in the radical times its target.

    source
    theorem ChainComplex.isMinimal_iff_range_d_succ_le_maximalIdeal_smul {R : Type u} [CommRing R] [IsLocalRing R] {K : ChainComplex (ModuleCat R) ℕ} :
    HomologicalComplex.IsMinimal K ↔ ∀ (n : ℕ), (ModuleCat.Hom.hom (K.d (n + 1) n)).range ≤ IsLocalRing.maximalIdeal R • ⊤

    Over a local ring, a natural-number-indexed chain complex is minimal exactly when each successive differential has image in the maximal ideal times its target.