Documentation

Mathlib.Algebra.Homology.Embedding.CochainComplex

Truncations on cochain complexes indexed by the integers. #

In this file, we introduce abbreviations for the canonical truncations CochainComplex.truncLE, CochainComplex.truncGE of cochain complexes indexed by ℤ, as well as the conditions CochainComplex.IsStrictlyLE, CochainComplex.IsStrictlyGE, CochainComplex.IsLE, and CochainComplex.IsGE.

source
@[reducible, inline]
noncomputable abbrev CochainComplex.truncLE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) :
CochainComplex C ℤ

If K : CochainComplex C ℤ, this is the canonical truncation ≤ n of K.

Equations
    Instances For
      source
      @[reducible, inline]
      noncomputable abbrev CochainComplex.truncGE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) :
      CochainComplex C ℤ

      If K : CochainComplex C ℤ, this is the canonical truncation ≥ n of K.

      Equations
        Instances For
          source
          noncomputable def CochainComplex.ιTruncLE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) :
          K.truncLE n ⟶ K

          The canonical map K.truncLE n ⟶ K for K : CochainComplex C ℤ.

          Equations
            Instances For
              source
              noncomputable def CochainComplex.πTruncGE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) :
              K ⟶ K.truncGE n

              The canonical map K ⟶ K.truncGE n for K : CochainComplex C ℤ.

              Equations
                Instances For
                  source
                  @[reducible, inline]
                  noncomputable abbrev CochainComplex.truncLEMap {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] [∀ (i : ℤ), HomologicalComplex.HasHomology L i] (n : ℤ) :
                  K.truncLE n ⟶ L.truncLE n

                  The morphism K.truncLE n ⟶ L.truncLE n induced by a morphism K ⟶ L.

                  Equations
                    Instances For
                      source
                      @[reducible, inline]
                      noncomputable abbrev CochainComplex.truncGEMap {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] [∀ (i : ℤ), HomologicalComplex.HasHomology L i] (n : ℤ) :
                      K.truncGE n ⟶ L.truncGE n

                      The morphism K.truncGE n ⟶ L.truncGE n induced by a morphism K ⟶ L.

                      Equations
                        Instances For
                          source
                          @[simp]
                          theorem CochainComplex.ιTruncLE_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] [∀ (i : ℤ), HomologicalComplex.HasHomology L i] (n : ℤ) :
                          CategoryTheory.CategoryStruct.comp (truncLEMap φ n) (L.ιTruncLE n) = CategoryTheory.CategoryStruct.comp (K.ιTruncLE n) φ
                          source
                          @[simp]
                          theorem CochainComplex.ιTruncLE_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] [∀ (i : ℤ), HomologicalComplex.HasHomology L i] (n : ℤ) {Z : CochainComplex C ℤ} (h : L ⟶ Z) :
                          CategoryTheory.CategoryStruct.comp (truncLEMap φ n) (CategoryTheory.CategoryStruct.comp (L.ιTruncLE n) h) = CategoryTheory.CategoryStruct.comp (K.ιTruncLE n) (CategoryTheory.CategoryStruct.comp φ h)
                          source
                          @[simp]
                          theorem CochainComplex.πTruncGE_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] [∀ (i : ℤ), HomologicalComplex.HasHomology L i] (n : ℤ) :
                          CategoryTheory.CategoryStruct.comp (K.πTruncGE n) (truncGEMap φ n) = CategoryTheory.CategoryStruct.comp φ (L.πTruncGE n)
                          source
                          @[simp]
                          theorem CochainComplex.πTruncGE_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] [∀ (i : ℤ), HomologicalComplex.HasHomology L i] (n : ℤ) {Z : CochainComplex C ℤ} (h : L.truncGE n ⟶ Z) :
                          CategoryTheory.CategoryStruct.comp (K.πTruncGE n) (CategoryTheory.CategoryStruct.comp (truncGEMap φ n) h) = CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp (L.πTruncGE n) h)
                          source
                          @[reducible, inline]
                          abbrev CochainComplex.IsStrictlyGE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n : ℤ) :
                          Prop

                          The condition that a cochain complex K is strictly ≥ n.

                          Equations
                            Instances For
                              source
                              @[reducible, inline]
                              abbrev CochainComplex.IsStrictlyLE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n : ℤ) :
                              Prop

                              The condition that a cochain complex K is strictly ≤ n.

                              Equations
                                Instances For
                                  source
                                  @[reducible, inline]
                                  abbrev CochainComplex.IsGE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n : ℤ) :
                                  Prop

                                  The condition that a cochain complex K is (cohomologically) ≥ n.

                                  Equations
                                    Instances For
                                      source
                                      @[reducible, inline]
                                      abbrev CochainComplex.IsLE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n : ℤ) :
                                      Prop

                                      The condition that a cochain complex K is (cohomologically) ≤ n.

                                      Equations
                                        Instances For
                                          source
                                          theorem CochainComplex.isZero_of_isStrictlyGE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n i : ℤ) (hi : i < n) [K.IsStrictlyGE n] :
                                          CategoryTheory.Limits.IsZero (K.X i)
                                          source
                                          theorem CochainComplex.isZero_of_isStrictlyLE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n i : ℤ) (hi : n < i) [K.IsStrictlyLE n] :
                                          CategoryTheory.Limits.IsZero (K.X i)
                                          source
                                          theorem CochainComplex.exactAt_of_isGE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n i : ℤ) (hi : i < n) [K.IsGE n] :
                                          HomologicalComplex.ExactAt K i
                                          source
                                          theorem CochainComplex.exactAt_of_isLE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n i : ℤ) (hi : n < i) [K.IsLE n] :
                                          HomologicalComplex.ExactAt K i
                                          source
                                          theorem CochainComplex.isZero_of_isGE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n i : ℤ) (hi : i < n) [K.IsGE n] [HomologicalComplex.HasHomology K i] :
                                          CategoryTheory.Limits.IsZero (HomologicalComplex.homology K i)
                                          source
                                          theorem CochainComplex.isZero_of_isLE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n i : ℤ) (hi : n < i) [K.IsLE n] [HomologicalComplex.HasHomology K i] :
                                          CategoryTheory.Limits.IsZero (HomologicalComplex.homology K i)
                                          source
                                          theorem CochainComplex.isStrictlyGE_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n : ℤ) :
                                          K.IsStrictlyGE n ↔ ∀ i < n, CategoryTheory.Limits.IsZero (K.X i)
                                          source
                                          theorem CochainComplex.isStrictlyLE_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n : ℤ) :
                                          K.IsStrictlyLE n ↔ ∀ (i : ℤ), n < i → CategoryTheory.Limits.IsZero (K.X i)
                                          source
                                          theorem CochainComplex.isGE_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n : ℤ) :
                                          K.IsGE n ↔ ∀ i < n, HomologicalComplex.ExactAt K i
                                          source
                                          theorem CochainComplex.isLE_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n : ℤ) :
                                          K.IsLE n ↔ ∀ (i : ℤ), n < i → HomologicalComplex.ExactAt K i
                                          source
                                          theorem CochainComplex.isStrictlyLE_of_le {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (p q : ℤ) (hpq : p ≤ q) [K.IsStrictlyLE p] :
                                          K.IsStrictlyLE q
                                          source
                                          theorem CochainComplex.isStrictlyGE_of_ge {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (p q : ℤ) (hpq : p ≤ q) [K.IsStrictlyGE q] :
                                          K.IsStrictlyGE p
                                          source
                                          theorem CochainComplex.isLE_of_le {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (p q : ℤ) (hpq : p ≤ q) [K.IsLE p] :
                                          K.IsLE q
                                          source
                                          theorem CochainComplex.isGE_of_ge {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (p q : ℤ) (hpq : p ≤ q) [K.IsGE q] :
                                          K.IsGE p
                                          source
                                          theorem CochainComplex.isStrictlyLE_of_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (e : K ≅ L) (n : ℤ) [K.IsStrictlyLE n] :
                                          L.IsStrictlyLE n
                                          source
                                          theorem CochainComplex.isStrictlyGE_of_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (e : K ≅ L) (n : ℤ) [K.IsStrictlyGE n] :
                                          L.IsStrictlyGE n
                                          source
                                          theorem CochainComplex.isLE_of_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (e : K ≅ L) (n : ℤ) [K.IsLE n] :
                                          L.IsLE n
                                          source
                                          theorem CochainComplex.isGE_of_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (e : K ≅ L) (n : ℤ) [K.IsGE n] :
                                          L.IsGE n
                                          source
                                          theorem CochainComplex.exists_iso_single {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] (n : ℤ) [K.IsStrictlyGE n] [K.IsStrictlyLE n] :
                                          ∃ (M : C), Nonempty (K ≅ (HomologicalComplex.single C (ComplexShape.up ℤ) n).obj M)

                                          A cochain complex that is both strictly ≤ n and ≥ n is isomorphic to a complex (single _ _ n).obj M for some object M.

                                          source
                                          instance CochainComplex.instIsStrictlyGEObjHomologicalComplexIntUpSingle {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (A : C) (n : ℤ) :
                                          IsStrictlyGE ((HomologicalComplex.single C (ComplexShape.up ℤ) n).obj A) n
                                          source
                                          instance CochainComplex.instIsStrictlyLEObjHomologicalComplexIntUpSingle {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (A : C) (n : ℤ) :
                                          IsStrictlyLE ((HomologicalComplex.single C (ComplexShape.up ℤ) n).obj A) n
                                          source
                                          instance CochainComplex.instIsIsoIntπTruncGEOfIsStrictlyGE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) [K.IsStrictlyGE n] :
                                          CategoryTheory.IsIso (K.πTruncGE n)
                                          source
                                          instance CochainComplex.instIsIsoIntιTruncLEOfIsStrictlyLE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) [K.IsStrictlyLE n] :
                                          CategoryTheory.IsIso (K.ιTruncLE n)
                                          source
                                          theorem CochainComplex.isIso_πTruncGE_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) :
                                          CategoryTheory.IsIso (K.πTruncGE n) ↔ K.IsStrictlyGE n
                                          source
                                          theorem CochainComplex.isIso_ιTruncLE_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) :
                                          CategoryTheory.IsIso (K.ιTruncLE n) ↔ K.IsStrictlyLE n
                                          source
                                          theorem CochainComplex.quasiIso_πTruncGE_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) :
                                          QuasiIso (K.πTruncGE n) ↔ K.IsGE n
                                          source
                                          theorem CochainComplex.quasiIso_ιTruncLE_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) :
                                          QuasiIso (K.ιTruncLE n) ↔ K.IsLE n
                                          source
                                          instance CochainComplex.instQuasiIsoIntπTruncGEOfIsGE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) [K.IsGE n] :
                                          QuasiIso (K.πTruncGE n)
                                          source
                                          instance CochainComplex.instQuasiIsoIntιTruncLEOfIsLE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) [K.IsLE n] :
                                          QuasiIso (K.ιTruncLE n)
                                          source
                                          theorem CochainComplex.quasiIso_truncGEMap_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] [∀ (i : ℤ), HomologicalComplex.HasHomology L i] (n : ℤ) :
                                          QuasiIso (truncGEMap φ n) ↔ ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i
                                          source
                                          theorem CochainComplex.quasiIso_truncLEMap_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] [∀ (i : ℤ), HomologicalComplex.HasHomology L i] (n : ℤ) :
                                          QuasiIso (truncLEMap φ n) ↔ ∀ i ≤ n, QuasiIsoAt φ i
                                          source
                                          instance CochainComplex.instIsStrictlyGEObjIntSingleFunctor {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (A : C) (n : ℤ) :
                                          ((singleFunctor C n).obj A).IsStrictlyGE n
                                          source
                                          instance CochainComplex.instIsStrictlyLEObjIntSingleFunctor {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (A : C) (n : ℤ) :
                                          ((singleFunctor C n).obj A).IsStrictlyLE n
                                          source
                                          theorem CochainComplex.isStrictlyLE_shift {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyLE n] (a n' : ℤ) (h : a + n' = n) :
                                          ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).IsStrictlyLE n'
                                          source
                                          theorem CochainComplex.isStrictlyGE_shift {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyGE n] (a n' : ℤ) (h : a + n' = n) :
                                          ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).IsStrictlyGE n'
                                          source
                                          theorem CochainComplex.isLE_shift {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) [CategoryTheory.CategoryWithHomology C] (n : ℤ) [K.IsLE n] (a n' : ℤ) (h : a + n' = n) :
                                          ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).IsLE n'
                                          source
                                          theorem CochainComplex.isGE_shift {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) [CategoryTheory.CategoryWithHomology C] (n : ℤ) [K.IsGE n] (a n' : ℤ) (h : a + n' = n) :
                                          ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).IsGE n'