Documentation

TauCeti.RingTheory.HochschildCohomology.Coboundary

The Hochschild coboundary with coefficients in a bimodule #

Let A be an algebra over a commutative semiring R and M an A-bimodule, written as a left A-module and a left Aᵐᵒᵖ-module whose actions commute, the right action of x being op x • m. A Hochschild n-cochain of A with coefficients in M is an R-multilinear map ψ : Aⁿ → M; the 0-cochains are the constant maps, i.e. the elements of M. This file constructs the Hochschild coboundary δ : Cⁿ(A, M) → Cⁿ⁺¹(A, M),

(δψ)(a₀, …, aₙ) = a₀ ψ(a₁, …, aₙ) + ∑_{j < n} (-1)ʲ⁺¹ ψ(a₀, …, aⱼaⱼ₊₁, …, aₙ) + (-1)ⁿ⁺¹ ψ(a₀, …, aₙ₋₁) aₙ,

as the alternating sum of its cofaces ∂ᵢ, proves the cosimplicial identities between the cofaces, and deduces δ ∘ δ = 0. The degree-zero cocycles are the central elements of M, the coboundary of m : M is the inner derivation a ↦ a m - m a, and the degree-one cocycles are the derivations A → M.

The degree of a cochain here is its number of arguments. The scalar cochains of TauCeti.RingTheory.CyclicCohomology.Cochain, whose coboundary b closes with the cyclic face (aₙ₊₁ a₀, a₁, …, aₙ), are instead indexed by one less than their number of arguments; they are the cochains with coefficients in the dual bimodule, see TauCeti.RingTheory.HochschildCohomology.Dual.

Main definitions #

Main results #

References #

source
def TauCeti.hochschildBimoduleCofaceFun {A : Type u_1} {M : Type u_2} [Semigroup A] {n : ℕ} (l r : A → M → M) (f : (Fin n → A) → M) (i : Fin (n + 2)) (a : Fin (n + 1) → A) :
M

The i-th Hochschild coface of a function f of n entries of A, valued in a type M with a left action l and a right action r of A: the zeroth coface is l (a 0) (f (a₁, …, aₙ)), the last coface is r aₙ (f (a₀, …, aₙ₋₁)), and the others multiply two adjacent entries. This is the formula shared by TauCeti.hochschildBimoduleCoface and its bounded analogue ContinuousLinearMap.hochschildBimoduleCoface; it needs no linear structure on M.

Instances For
    source
    @[simp]
    theorem TauCeti.hochschildBimoduleCofaceFun_zero {A : Type u_1} {M : Type u_2} [Semigroup A] {n : ℕ} (l r : A → M → M) (f : (Fin n → A) → M) (a : Fin (n + 1) → A) :
    hochschildBimoduleCofaceFun l r f 0 a = l (a 0) (f (Fin.tail a))

    The zeroth coface acts by the first entry on the left.

    source
    @[simp]
    theorem TauCeti.hochschildBimoduleCofaceFun_last {A : Type u_1} {M : Type u_2} [Semigroup A] {n : ℕ} (l r : A → M → M) (f : (Fin n → A) → M) (a : Fin (n + 1) → A) :
    hochschildBimoduleCofaceFun l r f (Fin.last (n + 1)) a = r (a (Fin.last n)) (f (Fin.init a))

    The last coface acts by the last entry on the right.

    source
    @[simp]
    theorem TauCeti.hochschildBimoduleCofaceFun_castSucc_succ {A : Type u_1} {M : Type u_2} [Semigroup A] {n : ℕ} (l r : A → M → M) (f : (Fin n → A) → M) (a : Fin (n + 1) → A) (j : Fin n) :
    hochschildBimoduleCofaceFun l r f j.castSucc.succ a = f (j.castSucc.contractNth (fun (x1 x2 : A) => x1 * x2) a)

    The inner cofaces multiply two adjacent entries.

    source
    theorem TauCeti.hochschildBimoduleCofaceFun_succ_castSucc {A : Type u_1} {M : Type u_2} [Semigroup A] {n : ℕ} (l r : A → M → M) (f : (Fin n → A) → M) (a : Fin (n + 1) → A) (j : Fin n) :
    hochschildBimoduleCofaceFun l r f j.succ.castSucc a = f (j.castSucc.contractNth (fun (x1 x2 : A) => x1 * x2) a)

    The inner cofaces multiply two adjacent entries, with the index written as j.succ.castSucc rather than j.castSucc.succ.

    source
    theorem TauCeti.hochschildBimoduleCofaceFun_hochschildBimoduleCofaceFun {A : Type u_1} {M : Type u_2} [Semigroup A] {n : ℕ} {l r : A → M → M} (f : (Fin n → A) → M) (hl : ∀ (a b : A) (x : M), l (a * b) x = l a (l b x)) (hr : ∀ (a b : A) (x : M), r (a * b) x = r b (r a x)) (hlr : ∀ (a b : A) (x : M), l a (r b x) = r b (l a x)) {i j : Fin (n + 2)} (hij : i ≤ j) :
    hochschildBimoduleCofaceFun l r (hochschildBimoduleCofaceFun l r f i) j.succ = hochschildBimoduleCofaceFun l r (hochschildBimoduleCofaceFun l r f j) i.castSucc

    The cosimplicial identity ∂_{j+1} ∘ ∂ᵢ = ∂ᵢ ∘ ∂_j for i ≤ j between the coface formulas, for actions l and r satisfying l (a * b) = l a ∘ l b, r (a * b) = r b ∘ r a and l a ∘ r b = r b ∘ l a.

    source
    def TauCeti.hochschildBimoduleCoface (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [Module Aᵐᵒᵖ M] [IsScalarTower R A M] [IsScalarTower R Aᵐᵒᵖ M] {n : ℕ} (i : Fin (n + 2)) :
    ((Fin n → A) →ₘₗ[R] M) →ₗ[R] (Fin (n + 1) → A) →ₘₗ[R] M

    The i-th coface of a cochain with coefficients in a bimodule, sending a multilinear map ψ in n arguments to a multilinear map in n + 1 arguments: the zeroth coface multiplies by the first entry on the left, the last coface multiplies by the last entry on the right, and the others multiply two adjacent entries.

    Instances For
      source
      @[simp]
      theorem TauCeti.hochschildBimoduleCoface_zero_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [Module Aᵐᵒᵖ M] [IsScalarTower R A M] [IsScalarTower R Aᵐᵒᵖ M] {n : ℕ} (ψ : (Fin n → A) →ₘₗ[R] M) (a : Fin (n + 1) → A) :
      ((hochschildBimoduleCoface R A M 0) ψ) a = a 0 • ψ (Fin.tail a)

      The zeroth coface multiplies by the first entry on the left.

      source
      @[simp]
      theorem TauCeti.hochschildBimoduleCoface_last_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [Module Aᵐᵒᵖ M] [IsScalarTower R A M] [IsScalarTower R Aᵐᵒᵖ M] {n : ℕ} (ψ : (Fin n → A) →ₘₗ[R] M) (a : Fin (n + 1) → A) :
      ((hochschildBimoduleCoface R A M (Fin.last (n + 1))) ψ) a = MulOpposite.op (a (Fin.last n)) • ψ (Fin.init a)

      The last coface multiplies by the last entry on the right.

      source
      @[simp]
      theorem TauCeti.hochschildBimoduleCoface_castSucc_succ_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [Module Aᵐᵒᵖ M] [IsScalarTower R A M] [IsScalarTower R Aᵐᵒᵖ M] {n : ℕ} (j : Fin n) (ψ : (Fin n → A) →ₘₗ[R] M) (a : Fin (n + 1) → A) :
      ((hochschildBimoduleCoface R A M j.castSucc.succ) ψ) a = ψ (j.castSucc.contractNth (fun (x1 x2 : A) => x1 * x2) a)

      The inner cofaces multiply two adjacent entries.

      source
      theorem TauCeti.hochschildBimoduleCoface_succ_castSucc_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [Module Aᵐᵒᵖ M] [IsScalarTower R A M] [IsScalarTower R Aᵐᵒᵖ M] {n : ℕ} (j : Fin n) (ψ : (Fin n → A) →ₘₗ[R] M) (a : Fin (n + 1) → A) :
      ((hochschildBimoduleCoface R A M j.succ.castSucc) ψ) a = ψ (j.castSucc.contractNth (fun (x1 x2 : A) => x1 * x2) a)

      The inner cofaces multiply two adjacent entries, with the index written as j.succ.castSucc rather than j.castSucc.succ.

      source
      theorem TauCeti.hochschildBimoduleCoface_hochschildBimoduleCoface {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [Module Aᵐᵒᵖ M] [IsScalarTower R A M] [IsScalarTower R Aᵐᵒᵖ M] {n : ℕ} [SMulCommClass A Aᵐᵒᵖ M] {i j : Fin (n + 2)} (hij : i ≤ j) (ψ : (Fin n → A) →ₘₗ[R] M) :
      (hochschildBimoduleCoface R A M j.succ) ((hochschildBimoduleCoface R A M i) ψ) = (hochschildBimoduleCoface R A M i.castSucc) ((hochschildBimoduleCoface R A M j) ψ)

      The cosimplicial identity ∂_{j+1} ∘ ∂ᵢ = ∂ᵢ ∘ ∂_j for i ≤ j.

      source
      def TauCeti.hochschildBimoduleCoboundary (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [Module Aᵐᵒᵖ M] [IsScalarTower R A M] [IsScalarTower R Aᵐᵒᵖ M] (n : ℕ) :
      ((Fin n → A) →ₘₗ[R] M) →ₗ[R] (Fin (n + 1) → A) →ₘₗ[R] M

      The Hochschild coboundary δ on cochains with coefficients in a bimodule M, the alternating sum ∑ᵢ (-1)ⁱ ∂ᵢ of the cofaces. Explicitly (hochschildBimoduleCoboundary_apply_eq_add_sum_add), `(δψ)(a₀, …, aₙ) = a₀ ψ(a₁, …, aₙ) + ∑_{j < n} (-1)ʲ⁺¹ ψ(a₀, …, aⱼaⱼ₊₁, …, aₙ)

      • (-1)ⁿ⁺¹ ψ(a₀, …, aₙ₋₁) aₙ`.
      Instances For
        source
        @[simp]
        theorem TauCeti.hochschildBimoduleCoboundary_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [Module Aᵐᵒᵖ M] [IsScalarTower R A M] [IsScalarTower R Aᵐᵒᵖ M] {n : ℕ} (ψ : (Fin n → A) →ₘₗ[R] M) (a : Fin (n + 1) → A) :
        ((hochschildBimoduleCoboundary R A M n) ψ) a = ∑ i : Fin (n + 2), (-1) ^ ↑i • ((hochschildBimoduleCoface R A M i) ψ) a

        The coboundary evaluates as the alternating sum of the cofaces.

        source
        theorem TauCeti.hochschildBimoduleCoboundary_apply_eq_add_sum_add {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [Module Aᵐᵒᵖ M] [IsScalarTower R A M] [IsScalarTower R Aᵐᵒᵖ M] {n : ℕ} (ψ : (Fin n → A) →ₘₗ[R] M) (a : Fin (n + 1) → A) :
        ((hochschildBimoduleCoboundary R A M n) ψ) a = a 0 • ψ (Fin.tail a) + ∑ j : Fin n, (-1) ^ (↑j + 1) • ψ (j.castSucc.contractNth (fun (x1 x2 : A) => x1 * x2) a) + (-1) ^ (n + 1) • MulOpposite.op (a (Fin.last n)) • ψ (Fin.init a)

        The Hochschild coboundary with coefficients in a bimodule, in explicit form.

        source
        @[simp]
        theorem TauCeti.hochschildBimoduleCoboundary_hochschildBimoduleCoboundary {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [Module Aᵐᵒᵖ M] [IsScalarTower R A M] [IsScalarTower R Aᵐᵒᵖ M] {n : ℕ} [SMulCommClass A Aᵐᵒᵖ M] (ψ : (Fin n → A) →ₘₗ[R] M) :
        (hochschildBimoduleCoboundary R A M (n + 1)) ((hochschildBimoduleCoboundary R A M n) ψ) = 0

        The Hochschild coboundary with coefficients in a bimodule squares to zero.

        source
        theorem TauCeti.hochschildBimoduleCoboundary_comp_hochschildBimoduleCoboundary {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [Module Aᵐᵒᵖ M] [IsScalarTower R A M] [IsScalarTower R Aᵐᵒᵖ M] {n : ℕ} [SMulCommClass A Aᵐᵒᵖ M] :
        hochschildBimoduleCoboundary R A M (n + 1) ∘ₗ hochschildBimoduleCoboundary R A M n = 0

        The Hochschild coboundary with coefficients in a bimodule squares to zero, as a composite of linear maps.

        source
        theorem TauCeti.hochschildBimoduleCoboundary_constOfIsEmpty {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [Module Aᵐᵒᵖ M] [IsScalarTower R A M] [IsScalarTower R Aᵐᵒᵖ M] (m : M) (a : Fin 1 → A) :
        ((hochschildBimoduleCoboundary R A M 0) (MultilinearMap.constOfIsEmpty R (fun (x : Fin 0) => A) m)) a = a 0 • m - MulOpposite.op (a 0) • m

        The coboundary of the degree-zero cochain with value m is the inner derivation a ↦ a • m - m • a.

        source
        theorem TauCeti.hochschildBimoduleCoboundary_constOfIsEmpty_eq_zero_iff {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [Module Aᵐᵒᵖ M] [IsScalarTower R A M] [IsScalarTower R Aᵐᵒᵖ M] (m : M) :
        (hochschildBimoduleCoboundary R A M 0) (MultilinearMap.constOfIsEmpty R (fun (x : Fin 0) => A) m) = 0 ↔ ∀ (x : A), x • m = MulOpposite.op x • m

        A degree-zero cochain is a cocycle exactly when its value lies in the centre of the bimodule.

        source
        theorem TauCeti.hochschildBimoduleCoboundary_ofSubsingleton {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [Module Aᵐᵒᵖ M] [IsScalarTower R A M] [IsScalarTower R Aᵐᵒᵖ M] (f : A →ₗ[R] M) (a : Fin 2 → A) :
        ((hochschildBimoduleCoboundary R A M 1) ((MultilinearMap.ofSubsingleton R A M 0) f)) a = a 0 • f (a 1) - f (a 0 * a 1) + MulOpposite.op (a 1) • f (a 0)

        The coboundary of a degree-one cochain f: (δf)(a₀, a₁) = a₀ • f a₁ - f (a₀ a₁) + f a₀ • a₁.

        source
        theorem TauCeti.hochschildBimoduleCoboundary_ofSubsingleton_eq_zero_iff {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [Module Aᵐᵒᵖ M] [IsScalarTower R A M] [IsScalarTower R Aᵐᵒᵖ M] (f : A →ₗ[R] M) :
        (hochschildBimoduleCoboundary R A M 1) ((MultilinearMap.ofSubsingleton R A M 0) f) = 0 ↔ ∀ (x y : A), f (x * y) = x • f y + MulOpposite.op y • f x

        A degree-one cochain is a cocycle exactly when it satisfies the Leibniz rule f (x y) = x • f y + f x • y, i.e. when it is a derivation into the bimodule in the sense of TauCeti.BimoduleDerivation.

        source
        theorem TauCeti.BimoduleDerivation.hochschildBimoduleCoboundary_ofSubsingleton_eq_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [Module Aᵐᵒᵖ M] [IsScalarTower R A M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass A Aᵐᵒᵖ M] (D : BimoduleDerivation R A M) :
        (hochschildBimoduleCoboundary R A M 1) ((MultilinearMap.ofSubsingleton R A M 0) D.toLinearMap) = 0

        A derivation into the bimodule is a degree-one Hochschild cocycle.