Documentation

TauCeti.RepresentationTheory.Homological.ContCohomology.ProjectionFormula

The projection formula for the explicit low-degree cup products #

The corestriction of a finite-index subgroup U ≤ G is not linear over the cohomology of G, but it is a map of modules over it: restricting a class of G to U, cupping there, and corestricting back is the same as cupping with the corestricted class. That is the projection formula

cor (res a ⌣ b) = a ⌣ cor b,        cor (b ⌣ res n) = cor b ⌣ n,

proved here in all six low-degree shapes.

In the five shapes with a degree-0 factor that factor is invariant, so partial application of the pairing at it is an equivariant additive map — TauCeti.ContCohomology.pairingLeft in the first display and TauCeti.ContCohomology.pairingRight in the second — and the cup with a degree-0 class is the coefficient map that equivariant map induces. In positive degrees the projection formula is therefore exactly naturality of the corestriction cochain in an equivariant coefficient map, TauCeti.ContCohomology.map_cochainsCor1 and map_cochainsCor2, and in those five shapes it holds already on cochains, with no coboundary correction. Those two cochain identities are stated for a variable transversal, so the statements below transport to any other transversal through TauCeti.ContCohomology.explicitCor1_eq_transversal and explicitCor2_eq_transversal. In the (1,0) and (2,0) shapes the translation factors g • and (g * h) • of the cup formula are absorbed by the invariance of the degree-0 factor before that naturality is applied; in degree 0 the same absorption is TauCeti.ContCohomology.pairingLeft_smul applied to each summand of the norm.

The (1,1) shape, the one shape of the six without a degree-0 factor, is the one shape where the two sides do not agree on cochains: the degree-two corestriction pairs the transversal word of the first variable with the translated transversal word of the second, so the two sides differ by a coboundary. That coboundary is exhibited by the explicit 1-cochain TauCeti.ContCohomology.cup11ProjectionHomotopy,

kᵗ(γ) = ∑ u : G ⧸ U, μ (a (t u)) (t u • b (ℓᵗ_u γ)),

whose d¹ is the difference of the two sides (TauCeti.ContCohomology.cup11ProjectionHomotopy_spec); the identity on classes follows.

Main statements #

References #

The degree-zero shape #

H⁰ is a subgroup and not a quotient, so neither a topology on G nor continuity of the pairing is involved.

source
theorem TauCeti.ContCohomology.explicitCup_projection00 (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (N : Type w) [AddCommGroup N] [DistribMulAction G N] (P : Type x) [AddCommGroup P] [DistribMulAction G P] (U : Subgroup G) [U.FiniteIndex] (μ : M →+ N →+ P) (hequiv : ∀ (g : G) (m : M) (y : N), (μ (g • m)) (g • y) = g • (μ m) y) (a : ↥(H0 G M)) (n : ↥(H0 (↥U) N)) :
(explicitCor0 G P U) (((explicitCup00 (↥U) M N P μ ⋯) ((explicitRes0 G M U) a)) n) = ((explicitCup00 G M N P μ hequiv) a) ((explicitCor0 G N U) n)

The (0,0) projection formula, cor⁰ (res⁰ a ⌣ n) = a ⌣ cor⁰ n: the norm of a pairing with a G-invariant first argument is that pairing applied to the norm. The whole content is that the transversal factors cross the pairing, which is TauCeti.ContCohomology.pairingLeft_smul.

The degree-one shapes #

Openness of U enters exactly as in TauCeti.ContCohomology.explicitCor1: it is what makes the corestriction of a continuous cochain continuous.

source
theorem TauCeti.ContCohomology.explicitCup_projection (G : Type u) [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [DistribMulAction G M] (N : Type w) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] (P : Type x) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] (U : Subgroup G) [U.FiniteIndex] (hU : IsOpen ↑U) (μ : M →+ N →+ P) (hμ : Continuous fun (p : M × N) => (μ p.1) p.2) (hequiv : ∀ (g : G) (m : M) (y : N), (μ (g • m)) (g • y) = g • (μ m) y) (a : ↥(H0 G M)) (b : H1 (↥U) N) :
(explicitCor1 G P U hU) (((explicitCup01 (↥U) M N P μ hμ ⋯) ((explicitRes0 G M U) a)) b) = ((explicitCup01 G M N P μ hμ hequiv) a) ((explicitCor1 G N U hU) b)

The (0,1) projection formula, cor¹ (res⁰ a ⌣ b) = a ⌣ cor¹ b for an open subgroup U of finite index.

source
theorem TauCeti.ContCohomology.explicitCup_projection10 (G : Type u) [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Type w) [AddCommGroup N] [TopologicalSpace N] [DistribMulAction G N] (P : Type x) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] (U : Subgroup G) [U.FiniteIndex] (hU : IsOpen ↑U) (μ : M →+ N →+ P) (hμ : Continuous fun (p : M × N) => (μ p.1) p.2) (hequiv : ∀ (g : G) (m : M) (y : N), (μ (g • m)) (g • y) = g • (μ m) y) (b : H1 (↥U) M) (n : ↥(H0 G N)) :
(explicitCor1 G P U hU) (((explicitCup10 (↥U) M N P μ hμ ⋯) b) ((explicitRes0 G N U) n)) = ((explicitCup10 G M N P μ hμ hequiv) ((explicitCor1 G M U hU) b)) n

The (1,0) projection formula, cor¹ (b ⌣ res⁰ n) = cor¹ b ⌣ n. The translation factors of the (1,0) cochain formula act trivially on the invariant n, which is what leaves a plain naturality statement behind.

The degree-two shapes #

The 2-cochains of the subgroup are functions on U × U, so the cup products over U need U to be a topological group. Degree one needs separately continuous multiplication on G; degree two uses [IsTopologicalGroup G] to obtain the corresponding structure on U.

source
theorem TauCeti.ContCohomology.explicitCup_projection02 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [DistribMulAction G M] (N : Type w) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] (P : Type x) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] (U : Subgroup G) [U.FiniteIndex] (hU : IsOpen ↑U) (μ : M →+ N →+ P) (hμ : Continuous fun (p : M × N) => (μ p.1) p.2) (hequiv : ∀ (g : G) (m : M) (y : N), (μ (g • m)) (g • y) = g • (μ m) y) (a : ↥(H0 G M)) (b : H2 (↥U) N) :
(explicitCor2 G P U hU) (((explicitCup02 (↥U) M N P μ hμ ⋯) ((explicitRes0 G M U) a)) b) = ((explicitCup02 G M N P μ hμ hequiv) a) ((explicitCor2 G N U hU) b)

The (0,2) projection formula, cor² (res⁰ a ⌣ b) = a ⌣ cor² b.

source
theorem TauCeti.ContCohomology.explicitCup_projection20 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Type w) [AddCommGroup N] [TopologicalSpace N] [DistribMulAction G N] (P : Type x) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] (U : Subgroup G) [U.FiniteIndex] (hU : IsOpen ↑U) (μ : M →+ N →+ P) (hμ : Continuous fun (p : M × N) => (μ p.1) p.2) (hequiv : ∀ (g : G) (m : M) (y : N), (μ (g • m)) (g • y) = g • (μ m) y) (b : H2 (↥U) M) (n : ↥(H0 G N)) :
(explicitCor2 G P U hU) (((explicitCup20 (↥U) M N P μ hμ ⋯) b) ((explicitRes0 G N U) n)) = ((explicitCup20 G M N P μ hμ hequiv) ((explicitCor2 G M U hU) b)) n

The (2,0) projection formula, cor² (b ⌣ res⁰ n) = cor² b ⌣ n.

The (1,1) homotopy #

The (1,1) shape is the one shape of the six in which neither factor is invariant, and the two sides of the projection formula are genuinely different cochains. Their difference is a coboundary, and this section writes down a primitive for it. Nothing here needs a topology: the identity TauCeti.ContCohomology.cup11ProjectionHomotopy_spec is an identity of plain cochains, just like the corestriction cochain identities it is proved from.

source
noncomputable def TauCeti.ContCohomology.cup11ProjectionHomotopy (G : Type u) [Group G] (M : Type v) [AddCommGroup M] (N : Type w) [AddCommGroup N] [DistribMulAction G N] (P : Type x) [AddCommGroup P] (U : Subgroup G) [U.FiniteIndex] (μ : M →+ N →+ P) (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (α : G → M) (β : ↥U → N) (γ : G) :
P

The (1,1) projection-formula homotopy for a transversal t,

kᵗ(γ) = ∑ u : G ⧸ U, μ (α (t u)) (t u • β (ℓᵗ_u γ)),

where ℓᵗ is the transversal word TauCeti.lWord. It is the corestriction sum of the pairing of α against β, evaluated at the transversal representatives in the first variable and at the transversal words in the second. Its d¹ is the difference of the two sides of the (1,1) projection formula, TauCeti.ContCohomology.cup11ProjectionHomotopy_spec.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.ContCohomology.cup11ProjectionHomotopy_apply (G : Type u) [Group G] (M : Type v) [AddCommGroup M] (N : Type w) [AddCommGroup N] [DistribMulAction G N] (P : Type x) [AddCommGroup P] (U : Subgroup G) [U.FiniteIndex] (μ : M →+ N →+ P) (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (α : G → M) (β : ↥U → N) (γ : G) :
    cup11ProjectionHomotopy G M N P U μ t ht α β γ = ∑ u : G ⧸ U, (μ (α (t u))) (t u • β ⟨lWord U t u γ, ⋯⟩)

    The defining formula for the (1,1) projection-formula homotopy.

    source
    theorem TauCeti.ContCohomology.cup11ProjectionHomotopy_spec (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (N : Type w) [AddCommGroup N] [DistribMulAction G N] (P : Type x) [AddCommGroup P] [DistribMulAction G P] (U : Subgroup G) [U.FiniteIndex] (μ : M →+ N →+ P) (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hequiv : ∀ (g : G) (m : M) (y : N), (μ (g • m)) (g • y) = g • (μ m) y) {α : G → M} (hα : groupCohomology.IsCocycle₁ α) {β : ↥U → N} (hβ : groupCohomology.IsCocycle₁ β) (γ η : G) :
    γ • cup11ProjectionHomotopy G M N P U μ t ht α β η - cup11ProjectionHomotopy G M N P U μ t ht α β (γ * η) + cup11ProjectionHomotopy G M N P U μ t ht α β γ = (cochainsCor2 G P U t ht) (fun (q : ↥U × ↥U) => (μ (α ↑q.1)) (↑q.1 • β q.2)) (γ, η) - (μ (α γ)) (γ • (cochainsCor1 G N U t ht) β η)

    The (1,1) projection formula on cochains, up to the explicit coboundary. For a 1-cocycle α of G and a 1-cocycle β of U, the difference between the corestriction of the cup of α|_U with β and the cup of α with the corestriction of β is d¹ of TauCeti.ContCohomology.cup11ProjectionHomotopy.

    The (1,1) shape #

    Continuity of the homotopy is what makes it a primitive in B², which is the image of the continuous 1-cochains, and it comes — as everywhere in this file — from openness of U through TauCeti.continuous_lWord.

    source
    theorem TauCeti.ContCohomology.continuous_cup11ProjectionHomotopy (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] (N : Type w) [AddCommGroup N] [TopologicalSpace N] [DistribMulAction G N] [ContinuousSMul G N] (P : Type x) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] (U : Subgroup G) [U.FiniteIndex] (hU : IsOpen ↑U) (μ : M →+ N →+ P) (hμ : Continuous fun (p : M × N) => (μ p.1) p.2) (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (α : G → M) {β : ↥U → N} (hβ : Continuous β) :
    Continuous (cup11ProjectionHomotopy G M N P U μ t ht α β)

    The (1,1) projection-formula homotopy of continuous data is continuous. As for the corestriction cochains themselves, no continuity is required of the transversal t.

    source
    theorem TauCeti.ContCohomology.explicitCup_projection11 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Type w) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] (P : Type x) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] (U : Subgroup G) [U.FiniteIndex] (hU : IsOpen ↑U) (μ : M →+ N →+ P) (hμ : Continuous fun (p : M × N) => (μ p.1) p.2) (hequiv : ∀ (g : G) (m : M) (y : N), (μ (g • m)) (g • y) = g • (μ m) y) (a : H1 G M) (b : H1 (↥U) N) :
    (explicitCor2 G P U hU) (((explicitCup11 (↥U) M N P μ hμ ⋯) ((explicitRes1 G M U) a)) b) = ((explicitCup11 G M N P μ hμ hequiv) a) ((explicitCor1 G N U hU) b)

    The (1,1) projection formula, cor² (res¹ a ⌣ b) = a ⌣ cor¹ b. Unlike the five shapes with a degree-0 factor, this one is not an identity of cochains: the two sides differ by d¹ of TauCeti.ContCohomology.cup11ProjectionHomotopy, which is TauCeti.ContCohomology.cup11ProjectionHomotopy_spec.

    Restricting the positive-degree factor: the homotopies #

    In the (1,0) and (2,0) shapes above the restricted factor is the invariant one. With the restriction on the cocycle instead, cor (res a ⌣ n) = a ⌣ cor⁰ n, the two sides again differ on cochains, and this section writes down the primitives. As for the (1,1) homotopy, nothing here needs a topology.

    The invariance of n under U is what makes every translate (t u * ℓᵗ_u γ) • n equal to t u • n, so that all the sums below have the fixed second pairing argument t u • n; what moves is only the first argument, and there the cocycle law of α does the work.

    source
    noncomputable def TauCeti.ContCohomology.cup10ProjectionHomotopy (G : Type u) [Group G] (M : Type v) [AddCommGroup M] (N : Type w) [AddCommGroup N] [DistribMulAction G N] (P : Type x) [AddCommGroup P] (U : Subgroup G) [U.FiniteIndex] (μ : M →+ N →+ P) (t : G ⧸ U → G) (α : G → M) (n : N) :
    P

    The (1,0) projection-formula homotopy for restriction on the cocycle factor and a transversal t, the 0-cochain ∑ u : G ⧸ U, μ (α (t u)) (t u • n). Its d⁰ is the difference of the two sides of cor¹ (res¹ α ⌣ n) = α ⌣ cor⁰ n, TauCeti.ContCohomology.cup10ProjectionHomotopy_spec.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.ContCohomology.cup10ProjectionHomotopy_apply (G : Type u) [Group G] (M : Type v) [AddCommGroup M] (N : Type w) [AddCommGroup N] [DistribMulAction G N] (P : Type x) [AddCommGroup P] (U : Subgroup G) [U.FiniteIndex] (μ : M →+ N →+ P) (t : G ⧸ U → G) (α : G → M) (n : N) :
      cup10ProjectionHomotopy G M N P U μ t α n = ∑ u : G ⧸ U, (μ (α (t u))) (t u • n)

      The defining formula for the (1,0) projection-formula homotopy.

      source
      noncomputable def TauCeti.ContCohomology.cup20ProjectionHomotopy (G : Type u) [Group G] (M : Type v) [AddCommGroup M] (N : Type w) [AddCommGroup N] [DistribMulAction G N] (P : Type x) [AddCommGroup P] (U : Subgroup G) [U.FiniteIndex] (μ : M →+ N →+ P) (t : G ⧸ U → G) (α : G × G → M) (n : N) (γ : G) :
      P

      The (2,0) projection-formula homotopy for restriction on the cocycle factor and a transversal t,

      kᵗ(γ) = ∑ u : G ⧸ U, μ (α (t u, ℓᵗ_u γ) - α (γ, t (γ⁻¹ • u))) (t u • n),

      where ℓᵗ is the transversal word TauCeti.lWord. Its d¹ is the difference of the two sides of cor² (res² α ⌣ n) = α ⌣ cor⁰ n, TauCeti.ContCohomology.cup20ProjectionHomotopy_spec.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.ContCohomology.cup20ProjectionHomotopy_apply (G : Type u) [Group G] (M : Type v) [AddCommGroup M] (N : Type w) [AddCommGroup N] [DistribMulAction G N] (P : Type x) [AddCommGroup P] (U : Subgroup G) [U.FiniteIndex] (μ : M →+ N →+ P) (t : G ⧸ U → G) (α : G × G → M) (n : N) (γ : G) :
        cup20ProjectionHomotopy G M N P U μ t α n γ = ∑ u : G ⧸ U, (μ (α (t u, lWord U t u γ) - α (γ, t (γ⁻¹ • u)))) (t u • n)

        The defining formula for the (2,0) projection-formula homotopy.

        source
        theorem TauCeti.ContCohomology.cup10ProjectionHomotopy_spec (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (N : Type w) [AddCommGroup N] [DistribMulAction G N] (P : Type x) [AddCommGroup P] [DistribMulAction G P] (U : Subgroup G) [U.FiniteIndex] (μ : M →+ N →+ P) (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hequiv : ∀ (g : G) (m : M) (y : N), (μ (g • m)) (g • y) = g • (μ m) y) {α : G → M} (hα : groupCohomology.IsCocycle₁ α) {n : N} (hn : n ∈ H0 (↥U) N) (γ : G) :
        γ • cup10ProjectionHomotopy G M N P U μ t α n - cup10ProjectionHomotopy G M N P U μ t α n = (cochainsCor1 G P U t ht) (fun (u : ↥U) => (μ (α ↑u)) (↑u • n)) γ - (μ (α γ)) (γ • ∑ u : G ⧸ U, t u • n)

        The (1,0) projection formula with restriction on the cocycle, on cochains, up to the explicit coboundary. For a 1-cocycle α of G and a U-invariant n, the difference between the corestriction of the cup of α|_U with n and the cup of α with the norm of n is d⁰ of TauCeti.ContCohomology.cup10ProjectionHomotopy.

        source
        theorem TauCeti.ContCohomology.cup20ProjectionHomotopy_spec (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (N : Type w) [AddCommGroup N] [DistribMulAction G N] (P : Type x) [AddCommGroup P] [DistribMulAction G P] (U : Subgroup G) [U.FiniteIndex] (μ : M →+ N →+ P) (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hequiv : ∀ (g : G) (m : M) (y : N), (μ (g • m)) (g • y) = g • (μ m) y) {α : G × G → M} (hα : groupCohomology.IsCocycle₂ α) {n : N} (hn : n ∈ H0 (↥U) N) (γ η : G) :
        γ • cup20ProjectionHomotopy G M N P U μ t α n η - cup20ProjectionHomotopy G M N P U μ t α n (γ * η) + cup20ProjectionHomotopy G M N P U μ t α n γ = (cochainsCor2 G P U t ht) (fun (q : ↥U × ↥U) => (μ (α (↑q.1, ↑q.2))) (↑(q.1 * q.2) • n)) (γ, η) - (μ (α (γ, η))) ((γ * η) • ∑ u : G ⧸ U, t u • n)

        The (2,0) projection formula with restriction on the cocycle, on cochains, up to the explicit coboundary. For a 2-cocycle α of G and a U-invariant n, the difference between the corestriction of the cup of α|_U with n and the cup of α with the norm of n is d¹ of TauCeti.ContCohomology.cup20ProjectionHomotopy.

        Restricting the positive-degree factor #

        The two shapes (1,0) and (2,0) of the projection formula with the restriction on the cocycle factor, cor (res a ⌣ n) = a ⌣ cor⁰ n. Together with the six shapes above these give the projection formula with the restriction on the first factor in every bidegree (p, q) with p + q ≤ 2.

        source
        theorem TauCeti.ContCohomology.continuous_cup20ProjectionHomotopy (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] (N : Type w) [AddCommGroup N] [TopologicalSpace N] [DistribMulAction G N] (P : Type x) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] (U : Subgroup G) [U.FiniteIndex] (hU : IsOpen ↑U) (μ : M →+ N →+ P) (hμ : Continuous fun (p : M × N) => (μ p.1) p.2) (t : G ⧸ U → G) {α : G × G → M} (hα : Continuous α) (n : N) :
        Continuous (cup20ProjectionHomotopy G M N P U μ t α n)

        The (2,0) projection-formula homotopy of a continuous cocycle is continuous: the transversal word is continuous by TauCeti.continuous_lWord, and γ ↦ t (γ⁻¹ • u) is locally constant because U is open.

        source
        theorem TauCeti.ContCohomology.explicitCup_projection10_res_left (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Type w) [AddCommGroup N] [TopologicalSpace N] [DistribMulAction G N] (P : Type x) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] (U : Subgroup G) [U.FiniteIndex] (hU : IsOpen ↑U) (μ : M →+ N →+ P) (hμ : Continuous fun (p : M × N) => (μ p.1) p.2) (hequiv : ∀ (g : G) (m : M) (y : N), (μ (g • m)) (g • y) = g • (μ m) y) (a : H1 G M) (n : ↥(H0 (↥U) N)) :
        (explicitCor1 G P U hU) (((explicitCup10 (↥U) M N P μ hμ ⋯) ((explicitRes1 G M U) a)) n) = ((explicitCup10 G M N P μ hμ hequiv) a) ((explicitCor0 G N U) n)

        The (1,0) projection formula with restriction on the cocycle, cor¹ (res¹ a ⌣ n) = a ⌣ cor⁰ n. The two sides differ on cochains by d⁰ of TauCeti.ContCohomology.cup10ProjectionHomotopy, which is TauCeti.ContCohomology.cup10ProjectionHomotopy_spec.

        source
        theorem TauCeti.ContCohomology.explicitCup_projection20_res_left (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Type w) [AddCommGroup N] [TopologicalSpace N] [DistribMulAction G N] (P : Type x) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] (U : Subgroup G) [U.FiniteIndex] (hU : IsOpen ↑U) (μ : M →+ N →+ P) (hμ : Continuous fun (p : M × N) => (μ p.1) p.2) (hequiv : ∀ (g : G) (m : M) (y : N), (μ (g • m)) (g • y) = g • (μ m) y) (a : H2 G M) (n : ↥(H0 (↥U) N)) :
        (explicitCor2 G P U hU) (((explicitCup20 (↥U) M N P μ hμ ⋯) ((explicitRes2 G M U) a)) n) = ((explicitCup20 G M N P μ hμ hequiv) a) ((explicitCor0 G N U) n)

        The (2,0) projection formula with restriction on the cocycle, cor² (res² a ⌣ n) = a ⌣ cor⁰ n. The two sides differ on cochains by d¹ of TauCeti.ContCohomology.cup20ProjectionHomotopy, which is TauCeti.ContCohomology.cup20ProjectionHomotopy_spec.