CupProduct.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

33 declarations, 0 contain sorry, 0 declared as axioms

Cup products in continuous group cohomology

This file constructs the cup product on continuous group cohomology, via a cup product pairing on the coinduced resolutions.

Main definitions

ContRepresentation.cupZeroSucc f hp n: the degree-(0, n) cup product pairing on the coinduced resolutions induced by an intertwining map f : ρ1 →ⁱL linHom ρ2 ρ3.
ContRepresentation.cupSucc F hF: the inductive step of the cup product, turning an intertwining map π₁ →ⁱL linHom π₂ π₃ with jointly continuous underlying pairing into an intertwining map π₁.coind₁ →ⁱL linHom π₂ π₃.coind₁.
ContRepresentation.cupComplex: the degree-(m, n) cup product pairing on the coinduced resolutions, as a morphism (resolution' (of ρ1)).X m ⟶ iHom ((resolution' (of ρ2)).X n) ((resolution' (of ρ3)).X (m + n)).
ContinuousCohomology.cupCochain: the cup product pairing on homogeneous cochains.
ContinuousCohomology.cup: the cup product on continuous group cohomology, descending cupCochain to the quotients of the cocycles by the coboundaries via ContinuousCohomology.cohomologyIsoQuot.

Throughout, the intertwining map f is only assumed to have jointly continuous uncurried pairing (hp); this holds automatically when M1 is discrete (ContRepresentation.continuous_pair_of_discrete).

Main results

ContRepresentation.cupPair_d_comm and ContinuousCohomology.cup_d_comm: the Leibniz rule d (σ ∪ τ) = (d σ) ∪ τ + (-1) ^ m • (σ ∪ d τ) for the cup product, on the resolutions and on homogeneous cochains respectively.

TODO

Minimise the imports once the constructions are complete.

Imports (7)

Imported by 1 file

FLT.lean

def ContRepresentation.cupSucc Documented declaration: cupSucc line 100 source
Source documentation
The inductive step of the cup product: an intertwining map F : π₁ →ⁱL linHom π₂ π₃ whose underlying pairing (v, w) ↦ F v w is jointly continuous induces an intertwining map π₁.coind₁ →ⁱL linHom π₂ π₃.coind₁ sending σ and τ to x ↦ F (σ x) τ.
The joint continuity hypothesis hF cannot be dropped: for a general F the continuity of τ ↦ (x ↦ F (σ x) τ) would require an equicontinuity property of F on compact subsets of C(G, V). It is preserved by this construction (continuous_cupSucc_uncurry), which allows the construction to be iterated.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, IsTopologicalGroup, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, ContinuousMap, ContRepresentation.coind₁
Proof uses: ContIntertwiningMap.mk, ContinuousLinearMap.mk, LinearMap.mk, AddHom.mk, ContinuousMap.mk
95 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
def cupSucc (F : π₁ →ⁱL linHom π₂ π₃)
    (hF : Continuous fun p : V × W2 ↦ F p.1 p.2) :
    π₁.coind₁ →ⁱL linHom π₂ π₃.coind₁ where
…
```
Mentions: ContRepresentation.linHom
lemma ContRepresentation.cupSucc_apply_apply line 120 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, IsTopologicalGroup, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, ContinuousMap, Eq, ContRepresentation.coind₁ and 1 more
Proof uses: rfl
88 instances, coercions and auxiliary constants left out.
lemma ContRepresentation.continuous_cupSucc_uncurry The uncurried pairing of cupSucc F hF is again jointly continuous, so cupSucc can be iterated line 126 source
Source documentation
The uncurried pairing of cupSucc F hF is again jointly continuous, so cupSucc can be iterated.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, IsTopologicalGroup, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, ContinuousMap, ContRepresentation.coind₁, ContRepresentation.cupSucc
Proof uses: Continuous.comp, Function.comp, ContinuousMap.comp, ContinuousMap.prodSwap, ContinuousMap.prodMk, ContinuousMap.const, Prod.mk, ContinuousMap.mk, ContinuousMap.continuous_postcomp, ContinuousMap.continuous_prodMk_const, Continuous.prodMk, continuous_snd, continuous_fst
78 instances, coercions and auxiliary constants left out.
```
lemma continuous_cupSucc_uncurry (F : π₁ →ⁱL linHom π₂ π₃)
    (hF : Continuous fun p : V × W2 ↦ F p.1 p.2) :
    Continuous fun p : C(G, V) × W2 ↦ cupSucc F hF p.1 p.2 :=
…
```
Mentions: ContRepresentation.linHom, ContRepresentation.cupSucc
def ContRepresentation.cupZeroSuccAux The pairing resolutionX (of ρ2) n × M1 → resolutionX (of ρ3) n underlying the cup product, sending (y, v) to resolutionCLM (f v) n y, as a continuous map line 144 source
Source documentation
The pairing resolutionX (of ρ2) n × M1 → resolutionX (of ρ3) n underlying the cup product, sending (y, v) to resolutionCLM (f v) n y, as a continuous map. The joint continuity of the uncurried pairing of f propagates through the levels of the resolution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, ContinuousMap, TopRep.resolutionX and 1 more
Proof uses: ContinuousMap.mk, ContRepresentation.resolutionCLM
71 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
def cupZeroSuccAux (n : ℕ) : C(resolutionX (of ρ2) n × M1, resolutionX (of ρ3) n) :=
…
```
def ContRepresentation.cupZeroSucc Documented declaration: cupZeroSucc line 165 source
Source documentation
The degree-(0, n) cup product pairing: an intertwining map f : ρ1 →ⁱL linHom ρ2 ρ3 pairs a degree-0 cochain σ with a degree-n cochain τ by (σ ∪ τ) g = resolutionCLM (f (σ g)) n (τ g), intertwining the coinduced representations.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, ContinuousMap, TopRep.resolutionX and 5 more
Proof uses: ContIntertwiningMap.mk, ContinuousLinearMap.mk, LinearMap.mk, AddHom.mk, ContinuousMap.mk, ContRepresentation.resolutionCLM
112 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
def cupZeroSucc (n : ℕ) :
    ρ1.coind₁ →ⁱL linHom (resolutionX (of ρ2) (n + 1)).ρ (resolutionX (of ρ3) (n + 1)).ρ where
…
```
Mentions: ContRepresentation.linHom
lemma ContRepresentation.cupZeroSucc_apply_apply line 184 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, ContinuousMap, TopRep.resolutionX and 8 more
Proof uses: rfl
106 instances, coercions and auxiliary constants left out.
lemma ContRepresentation.continuous_cupZeroSucc_uncurry The uncurried pairing of cupZeroSucc f hp n is jointly continuous, so cupSucc applies to it line 189 source
Source documentation
The uncurried pairing of cupZeroSucc f hp n is jointly continuous, so cupSucc applies to it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, ContinuousMap, TopRep.resolutionX and 6 more
Proof uses: Continuous.comp, Function.comp, ContinuousMap.prodMk, Prod.mk, ContinuousMap.comp, ContRepresentation.cupZeroSuccAux, ContinuousMap.continuous_postcomp, ContinuousMap.continuous_prodMk, Continuous.prodMk, continuous_snd, continuous_fst
93 instances, coercions and auxiliary constants left out.
```
lemma continuous_cupZeroSucc_uncurry (n : ℕ) :
    Continuous fun p : C(G, M1) × C(G, resolutionX (of ρ2) n) ↦ cupZeroSucc f hp n p.1 p.2 :=
…
```
Mentions: ContRepresentation.cupZeroSucc
def ContRepresentation.cupPair Documented declaration: cupPair line 197 source
Source documentation
The degree-(m, n) cup product pairing on the coinduced resolutions, defined by iterating cupSucc starting from cupZeroSucc, bundled with the joint continuity of its underlying pairing (which is needed to keep iterating).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Subtype, TopRep.resolutionX and 4 more
91 instances, coercions and auxiliary constants left out.
```
def cupPair (n : ℕ) : (m : ℕ) →
    { F : (resolutionX (of ρ1) (m + 1)).ρ →ⁱL
        linHom (resolutionX (of ρ2) (n + 1)).ρ (resolutionX (of ρ3) (n + 1 + m)).ρ //
      Continuous fun p : ↥(resolutionX (of ρ1) (m + 1)) × ↥(resolutionX (of ρ2) (n + 1)) ↦
        F p.1 p.2 }
  | 0 => ⟨cupZeroSucc f hp n, continuous_cupZeroSucc_uncurry f hp n⟩
  | m + 1 =>
    ⟨cupSucc (cupPair n m).1 (cupPair n m).2,
      continuous_cupSucc_uncurry (cupPair n m).1 (cupPair n m).2⟩

end
```
Mentions: ContRepresentation.linHom, ContRepresentation.cupZeroSucc, ContRepresentation.continuous_cupZeroSucc_uncurry, ContRepresentation.cupSucc, ContRepresentation.continuous_cupSucc_uncurry
def ContRepresentation.cupComplex Documented declaration: cupComplex line 212 source
Source documentation
The degree-(m, n) cup product pairing on the coinduced resolutions, as a morphism from the m-th level to the internal hom of the n-th and r-th levels, obtained from cupPair by reindexing along r = m + n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 7 more
Proof uses: CategoryTheory.CategoryStruct.comp, TopRep.resolutionX, OfNat.ofNat, TopRep.ρ, TopRep.ofHom, ContRepresentation.cupPair, CategoryTheory.eqToHom
112 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def cupComplex (m n r : ℕ) (hr : r = m + n) :
    (TopRep.resolution' (.of ρ1)).X m ⟶
      iHom ((TopRep.resolution' (.of ρ2)).X n) ((TopRep.resolution' (.of ρ3)).X r) :=
…
```
lemma ContRepresentation.cupPair_zero line 224 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, TopRep.resolutionX and 6 more
Proof uses: rfl
90 instances, coercions and auxiliary constants left out.
lemma ContRepresentation.cupPair_succ_apply line 226 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, TopRep.resolutionX, TopRep.of and 6 more
Proof uses: rfl
92 instances, coercions and auxiliary constants left out.
lemma ContRepresentation.cupZeroSucc_const_apply Cupping with a constant 0-cochain acts through the functorial extension of f v line 231 source
Source documentation
Cupping with a constant 0-cochain acts through the functorial extension of f v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, TopRep.resolutionX, TopRep.of and 9 more
Proof uses: rfl
104 instances, coercions and auxiliary constants left out.
```
lemma cupZeroSucc_const_apply (n : ℕ) (v : M1) (τ : ↥(resolutionX (of ρ2) (n + 1))) :
    cupZeroSucc f hp n (ContinuousMap.const G v) τ = resolutionCLM ρ2 ρ3 (f v) (n + 1) τ := rfl
```
Mentions: ContRepresentation.cupZeroSucc, ContRepresentation.resolutionCLM
lemma ContRepresentation.cupPair_d_comm The Leibniz rule for the cup product pairing on the levels of the standard resolutions: d (σ ∪ τ) = (d σ) ∪ τ + (-1) ^ m • (σ ∪ d τ) line 236 source
Source documentation
The Leibniz rule for the cup product pairing on the levels of the standard resolutions: d (σ ∪ τ) = (d σ) ∪ τ + (-1) ^ m • (σ ∪ d τ).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, TopRep.resolutionX, TopRep.of and 13 more
Proof uses: Nat.recAux, ContinuousMap.ext, id, ContinuousMap, HSub.hSub, ContinuousMap.const, Eq.mpr, congrArg, ContRepresentation.d_hom_succ_apply, ContRepresentation.d_hom_zero, Eq.refl, Decidable.byContradiction, Not, ContRepresentation.resolutionCLM, rfl, ContRepresentation.cupZeroSucc, ContRepresentation.cupPair_zero, ContRepresentation.coind₁, ContRepresentation.cupZeroSucc_const_apply, ContRepresentation.resolutionCLM_comp_d and 11 more
173 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma cupPair_d_comm (n m : ℕ) (σ : ↥(resolutionX (of ρ1) (m + 1)))
    (τ : ↥(resolutionX (of ρ2) (n + 1))) :
    (d (of ρ3) (n + 1 + m)).hom ((cupPair f hp n m).1 σ τ) =
      (cupPair f hp n (m + 1)).1 ((d (of ρ1) (m + 1)).hom σ) τ +
        (-1 : ℤ) ^ m • resolutionXCast (.of ρ3) (by omega : n + 1 + 1 + m = n + 1 + m + 1)
          ((cupPair f hp (n + 1) m).1 σ ((d (of ρ2) (n + 1)).hom τ)) := by
…
```
Mentions: ContRepresentation.cupPair, ContRepresentation.resolutionXCast
abbrev ContinuousCohomology.cupCochain The cup product pairing on homogeneous cochains, obtained from the cup product pairing cupComplex on the coinduced resolutions by taking invariants line 311 source
Source documentation
The cup product pairing on homogeneous cochains, obtained from the cup product pairing cupComplex on the coinduced resolutions by taking invariants.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 7 more
Proof uses: CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.obj, TopRep, TopRep.invariantsFunctor, TopRep.iHom, TopRep.resolution', CategoryTheory.Functor.map, ContRepresentation.cupComplex, ContRepresentation.invariantsObjIHom
96 instances, coercions and auxiliary constants left out.
```
abbrev cupCochain (m n r : ℕ) (hr : r = m + n) :
    (homogeneousCochains (.of ρ1)).X m ⟶ TopModuleCat.linHom ((homogeneousCochains (.of ρ2)).X n)
      ((homogeneousCochains (.of ρ3)).X r) :=
…
```
Mentions: TopModuleCat.linHom
lemma ContinuousCohomology.cupCochain_coe The value of the cup product of two homogeneous cochains, as an element of the resolution line 320 source
Source documentation
The value of the cup product of two homogeneous cochains, as an element of the resolution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 19 more
Proof uses: Eq.rec, Eq.symm, ContRepresentation.eqToHom_iHom_apply, Decidable.byContradiction, Not, Eq.mpr, TopRep.iHom, id, congrArg, Eq.refl
140 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma cupCochain_coe (m n r : ℕ) (hr : r = m + n) (σ : (homogeneousCochains (.of ρ1)).X m)
    (τ : (homogeneousCochains (.of ρ2)).X n) :
    (cupCochain f hp m n r hr σ τ : ↥((of ρ3).resolution'.X r)) =
      resolutionXCast (.of ρ3) (by omega : n + 1 + m = r + 1)
        ((cupPair f hp n m).1 σ.1 τ.1) := by
…
```
Mentions: ContinuousCohomology.cupCochain
lemma ContinuousCohomology.cupCochain_apply_zero line 331 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 14 more
Proof uses: map_zero, RingHom
131 instances, coercions and auxiliary constants left out.
lemma ContinuousCohomology.cup_d_comm line 337 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 21 more
Proof uses: Eq.rec, Eq.symm, Subtype.ext, Membership.mem, Eq.refl, Eq.mpr, TopRep.Hom.hom, TopRep.d, id, congrArg, TopModuleCat.Hom.hom, TopRep.homogeneousCochains.d_apply, ContRepresentation.resolutionXCast, ContRepresentation.cupPair, ContinuousCohomology.cupCochain_coe, ContRepresentation.d_hom_resolutionXCast, Nat.add, ContRepresentation.cupPair_d_comm, map_add, map_zsmul and 6 more
192 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma ContinuousCohomology.cupCochain_zero_apply cupCochain vanishes when its first argument is zero line 351 source
Source documentation
cupCochain vanishes when its first argument is zero.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 14 more
Proof uses: id, congrArg, TopModuleCat.Hom.hom, TopRep.resolutionX, map_zero, RingHom
140 instances, coercions and auxiliary constants left out.
```
lemma cupCochain_zero_apply (m n r : ℕ) (hr : r = m + n)
    (τ : (homogeneousCochains (.of ρ2)).X n) :
    cupCochain f hp m n r hr 0 τ = 0 :=
…
```
Mentions: ContinuousCohomology.cupCochain
lemma ContinuousCohomology.d_cupCochain_eq_zero The cup product of two cocycles is a cocycle line 358 source
Source documentation
The cup product of two cocycles is a cocycle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 15 more
Proof uses: HSMul.hSMul, Int, Submodule, TopRep.resolutionX, HPow.hPow, Neg.neg, ContinuousCohomology.cup_d_comm, Eq.trans, Eq.mp, congrArg, ContinuousCohomology.cupCochain_apply_zero, ContinuousCohomology.cupCochain_zero_apply, of_eq_true, Subtype, ContinuousMap, Membership.mem, ContRepresentation.coind₁, True, congrFun', smul_zero and 2 more
156 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma d_cupCochain_eq_zero (m n r : ℕ) (hr : r = m + n)
    {σ : (homogeneousCochains (.of ρ1)).X m} {τ : (homogeneousCochains (.of ρ2)).X n}
    (hσ : (homogeneousCochains (.of ρ1)).d m (m + 1) σ = 0)
    (hτ : (homogeneousCochains (.of ρ2)).d n (n + 1) τ = 0) :
    (homogeneousCochains (.of ρ3)).d r (r + 1) (cupCochain f hp m n r hr σ τ) = 0 := by
…
```
Mentions: ContinuousCohomology.cupCochain
def ContinuousCohomology.cupKerCLM For a fixed cocycle σ, cupping with σ restricts to a continuous linear map between the kernels of the differentials on homogeneous cochains line 373 source
Source documentation
For a fixed cocycle σ, cupping with σ restricts to a continuous linear map between the kernels of the differentials on homogeneous cochains.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 18 more
Proof uses: ContinuousLinearMap.restrict, TopModuleCat.linHom, CategoryTheory.ConcreteCategory.hom, ContinuousCohomology.cupCochain
122 instances, coercions and auxiliary constants left out.
```
noncomputable def cupKerCLM (m n r : ℕ) (hr : r = m + n)
    (σ : ↥(TopModuleCat.ker ((homogeneousCochains (.of ρ1)).d m (m + 1)))) :
    ↥(TopModuleCat.ker ((homogeneousCochains (.of ρ2)).d n (n + 1))) →L[k]
      ↥(TopModuleCat.ker ((homogeneousCochains (.of ρ3)).d r (r + 1))) :=
…
```
lemma ContinuousCohomology.cupKerCLM_apply_coe line 383 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 22 more
Proof uses: rfl
138 instances, coercions and auxiliary constants left out.
lemma ContinuousCohomology.cupCochain_d_comp_d The cup product with a doubly-applied differential vanishes line 390 source
Source documentation
The cup product with a doubly-applied differential vanishes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 15 more
Proof uses: Eq.mpr, id, congrArg, TopRep.homogeneousCochains.d_comp_d_apply, map_zero, RingHom
138 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma cupCochain_d_comp_d (m i j l r : ℕ) (hr : r = m + l)
    (σ : (homogeneousCochains (.of ρ1)).X m) (τ : (homogeneousCochains (.of ρ2)).X i) :
    cupCochain f hp m l r hr σ
      ((homogeneousCochains (.of ρ2)).d j l ((homogeneousCochains (.of ρ2)).d i j τ)) = 0 := by
…
```
Mentions: ContinuousCohomology.cupCochain
lemma ContinuousCohomology.d_cup_d The cup product of two coboundaries is a coboundary: (d σ) ∪ (d τ) = d (σ ∪ d τ) line 403 source
Source documentation
The cup product of two coboundaries is a coboundary: (d σ) ∪ (d τ) = d (σ ∪ d τ). This is the special case of the Leibniz rule cup_d_comm where the second argument is a coboundary.
Note that (d σ) ∪ (d τ) is not zero in general: by the Leibniz rule it is the coboundary of σ ∪ d τ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 11 more
Proof uses: Eq.rec, Eq.symm, rfl, TopRep, TopRep.resolution', ContRepresentation.invariants, TopRep.ρ, HSMul.hSMul, Int, Submodule, TopRep.resolutionX, HPow.hPow, Neg.neg, ContinuousCohomology.cup_d_comm, id, Eq.refl, Eq.mp, Subtype, ContinuousMap, Membership.mem and 14 more
154 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma d_cup_d (m n r : ℕ) (hr : r = m + n) (σ : (homogeneousCochains (.of ρ1)).X m)
    (τ : (homogeneousCochains (.of ρ2)).X n) :
    cupCochain f hp (m + 1) (n + 1) (r + 2) (by omega)
      ((homogeneousCochains (.of ρ1)).d m (m + 1) σ)
      ((homogeneousCochains (.of ρ2)).d n (n + 1) τ) =
    (homogeneousCochains (.of ρ3)).d (r + 1) (r + 2) (cupCochain f hp m (n + 1) (r + 1) (by omega) σ
      ((homogeneousCochains (.of ρ2)).d n (n + 1) τ)) := by
…
```
Mentions: ContinuousCohomology.cupCochain
lemma ContinuousCohomology.d_cupCochain_of_d_eq_zero Cupping a coboundary with a cocycle gives a coboundary line 418 source
Source documentation
Cupping a coboundary with a cocycle gives a coboundary.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 15 more
Proof uses: HSMul.hSMul, Int, Submodule, TopRep.resolutionX, HPow.hPow, Neg.neg, ContinuousCohomology.cup_d_comm, of_eq_true, Subtype, ContinuousMap, Membership.mem, ContRepresentation.coind₁, Eq.trans, True, forall_congr, congrArg, smul_zero, add_zero, eq_self, implies_true and 3 more
157 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma d_cupCochain_of_d_eq_zero (m n r : ℕ) (hr : r = m + n)
    (σ : (homogeneousCochains (.of ρ1)).X m) {τ : (homogeneousCochains (.of ρ2)).X n}
    (hτ : (homogeneousCochains (.of ρ2)).d n (n + 1) τ = 0) :
    cupCochain f hp (m + 1) n (r + 1) (by omega) ((homogeneousCochains (.of ρ1)).d m (m + 1) σ) τ =
      (homogeneousCochains (.of ρ3)).d r (r + 1) (cupCochain f hp m n r hr σ τ) := by
…
```
Mentions: ContinuousCohomology.cupCochain
lemma ContinuousCohomology.cupCochain_d_of_d_eq_zero Cupping a cocycle with a coboundary gives a coboundary, up to the sign (-1) ^ m line 431 source
Source documentation
Cupping a cocycle with a coboundary gives a coboundary, up to the sign (-1) ^ m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 21 more
Proof uses: ContinuousCohomology.cup_d_comm, Eq.mpr, id, congrArg, Eq.mp, ContinuousCohomology.cupCochain_zero_apply, zero_add, HMul.hMul, smul_smul, Eq.symm, pow_add, Even.neg_one_pow, Exists.intro, rfl, one_smul, Eq.refl
185 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma cupCochain_d_of_d_eq_zero (m n r : ℕ) (hr : r = m + n)
    {σ : (homogeneousCochains (.of ρ1)).X m} (τ : (homogeneousCochains (.of ρ2)).X n)
    (hσ : (homogeneousCochains (.of ρ1)).d m (m + 1) σ = 0) :
    cupCochain f hp m (n + 1) (r + 1) (by omega) σ ((homogeneousCochains (.of ρ2)).d n (n + 1) τ) =
      (-1 : ℤ) ^ m • (homogeneousCochains (.of ρ3)).d r (r + 1) (cupCochain f hp m n r hr σ τ) := by
…
```
Mentions: ContinuousCohomology.cupCochain
lemma ContinuousCohomology.continuous_cupKerCLM_uncurry The cup product pairing on the kernels of the differentials is jointly continuous line 448 source
Source documentation
The cup product pairing on the kernels of the differentials is jointly continuous.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 19 more
Proof uses: Iff.mpr, TopologicalSpace.induced, Function.comp, continuous_induced_rng, id, TopModuleCat.linHom, CategoryTheory.ConcreteCategory.hom, ContinuousCohomology.cupCochain, ContRepresentation.resolutionXCast, Decidable.byContradiction, Not, ContRepresentation.cupPair, funext, ContinuousCohomology.cupCochain_coe, Eq.mpr, congrArg, Continuous.comp, ContinuousLinearMap.continuous, Subtype, Prod.mk and 5 more
141 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma continuous_cupKerCLM_uncurry (m n r : ℕ) (hr : r = m + n) :
    Continuous fun p : ↥(TopModuleCat.ker ((homogeneousCochains (.of ρ1)).d m (m + 1))) ×
        ↥(TopModuleCat.ker ((homogeneousCochains (.of ρ2)).d n (n + 1))) ↦
      cupKerCLM f hp m n r hr p.1 p.2 := by
…
```
Mentions: ContinuousCohomology.cupKerCLM
def ContinuousCohomology.cupKerHom The cup product bundled as a morphism from the kernel of the differential into the internal hom of the kernel models line 472 source
Source documentation
The cup product bundled as a morphism from the kernel of the differential into the internal hom of the kernel models.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 10 more
Proof uses: TopModuleCat.homOfBilinear, ContinuousCohomology.cupKerCLM, ContinuousCohomology.continuous_cupKerCLM_uncurry
96 instances, coercions and auxiliary constants left out.
```
noncomputable def cupKerHom (f : ρ1 →ⁱL ρ2.linHom ρ3) (hp : Continuous fun p : M1 × M2 ↦ f p.1 p.2)
    (m n r : ℕ) (hr : r = m + n) :
    TopModuleCat.ker ((homogeneousCochains (.of ρ1)).d m (m + 1)) ⟶
      TopModuleCat.linHom (TopModuleCat.ker ((homogeneousCochains (.of ρ2)).d n (n + 1)))
        (TopModuleCat.ker ((homogeneousCochains (.of ρ3)).d r (r + 1))) :=
…
```
Mentions: TopModuleCat.linHom
abbrev ContinuousCohomology.cupCocyclesAux The cup product of two cocycles, as a cocycle: by the Leibniz rule cup_d_comm, the differential of σ ∪ τ vanishes when d σ = 0 and d τ = 0 line 484 source
Source documentation
The cup product of two cocycles, as a cocycle: by the Leibniz rule cup_d_comm, the differential of σ ∪ τ vanishes when d σ = 0 and d τ = 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 7 more
Proof uses: TopModuleCat.ker, HomologicalComplex.X, OfNat.ofNat, HomologicalComplex.d, TopModuleCat.Hom.hom, CategoryTheory.Iso.inv, HomologicalComplex.cyclesIsoKer, Subtype.mk, Membership.mem, Submodule, LinearMap.ker, TopModuleCat.linHom, CategoryTheory.ConcreteCategory.hom, ContinuousCohomology.cupCochain, CategoryTheory.Iso.hom
107 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
noncomputable abbrev cupCocyclesAux (f : ρ1 →ⁱL ρ2.linHom ρ3)
    (hp : Continuous fun p : M1 × M2 ↦ f p.1 p.2) (m n r : ℕ) (hr : r = m + n)
    (σ : (homogeneousCochains (.of ρ1)).cycles m)
    (τ : (homogeneousCochains (.of ρ2)).cycles n) :
    (homogeneousCochains (.of ρ3)).cycles r :=
…
```
def ContinuousCohomology.cupCocycles The cup product pairing on the cycles of the homogeneous cochain complexes, transporting cupKerHom along the identification cyclesIsoKer of the cycles with the kernel models line 498 source
Source documentation
The cup product pairing on the cycles of the homogeneous cochain complexes, transporting cupKerHom along the identification cyclesIsoKer of the cycles with the kernel models.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 8 more
Proof uses: CategoryTheory.CategoryStruct.comp, TopModuleCat.ker, HomologicalComplex.X, OfNat.ofNat, HomologicalComplex.d, CategoryTheory.Iso.hom, HomologicalComplex.cyclesIsoKer, ContinuousCohomology.cupKerHom, TopModuleCat.linHomMap, CategoryTheory.Iso.inv
98 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
noncomputable def cupCocycles (f : ρ1 →ⁱL ρ2.linHom ρ3)
    (hp : Continuous fun p : M1 × M2 ↦ f p.1 p.2) (m n r : ℕ) (hr : r = m + n) :
    (homogeneousCochains (.of ρ1)).cycles m ⟶
      TopModuleCat.linHom ((homogeneousCochains (.of ρ2)).cycles n)
        ((homogeneousCochains (.of ρ3)).cycles r) :=
…
```
Mentions: TopModuleCat.linHom
lemma ContinuousCohomology.cupCocycles_apply line 511 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 11 more
Proof uses: rfl
110 instances, coercions and auxiliary constants left out.
lemma ContinuousCohomology.cokerπ_cupKerCLM_bdryKer_left Cupping a coboundary with a cocycle dies in the quotient by the coboundaries line 519 source
Source documentation
Cupping a coboundary with a cocycle dies in the quotient by the coboundaries.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 25 more
Proof uses: Nat.casesAuxOn, Subtype.ext, Eq.mpr, id, congrArg, ContinuousCohomology.bdryKer_apply_coe, Quiver.Hom, HomologicalComplex.shape, of_eq_true, Not, ComplexShape.Rel, Eq.trans, False, True, congrFun', zero_tsub, ComplexShape.up_Rel, zero_add, not_false_eq_true, Eq.refl and 42 more
203 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma cokerπ_cupKerCLM_bdryKer_left (m n r : ℕ) (hr : r = m + n)
    (y : ↥((homogeneousCochains (.of ρ1)).X (m - 1)))
    (τ : ↥(TopModuleCat.ker ((homogeneousCochains (.of ρ2)).d n (n + 1)))) :
    TopModuleCat.cokerπ (bdryKer (.of ρ3) r)
      (cupKerCLM f hp m n r hr (bdryKer (.of ρ1) m y) τ) = 0 := by
…
```
Mentions: ContinuousCohomology.bdryKer, ContinuousCohomology.cupKerCLM
lemma ContinuousCohomology.cokerπ_cupKerCLM_bdryKer_right Cupping a cocycle with a coboundary dies in the quotient by the coboundaries line 544 source
Source documentation
Cupping a cocycle with a coboundary dies in the quotient by the coboundaries.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 25 more
Proof uses: Nat.casesAuxOn, Subtype.ext, Eq.mpr, id, congrArg, ContinuousCohomology.bdryKer_apply_coe, Quiver.Hom, HomologicalComplex.shape, of_eq_true, Not, ComplexShape.Rel, Eq.trans, False, True, congrFun', zero_tsub, ComplexShape.up_Rel, zero_add, not_false_eq_true, Eq.refl and 19 more
191 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma cokerπ_cupKerCLM_bdryKer_right (m n r : ℕ) (hr : r = m + n)
    (σ : ↥(TopModuleCat.ker ((homogeneousCochains (.of ρ1)).d m (m + 1))))
    (y : ↥((homogeneousCochains (.of ρ2)).X (n - 1))) :
    TopModuleCat.cokerπ (bdryKer (.of ρ3) r)
      (cupKerCLM f hp m n r hr σ (bdryKer (.of ρ2) n y)) = 0 := by
…
```
Mentions: ContinuousCohomology.bdryKer, ContinuousCohomology.cupKerCLM
def ContinuousCohomology.cup Documented declaration: cup line 570 source
Source documentation
The cup product on continuous group cohomology induced by an intertwining map f : ρ1 →ⁱL linHom ρ2 ρ3: descend the kernel-model cup product cupKerHom to the quotients by the coboundaries on all three slots, and transport along cohomologyIsoQuot.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContIntertwiningMap, ContinuousLinearMap, RingHom.id, ContRepresentation.linHom, Continuous, Prod, Prod.fst, Prod.snd, Nat, Eq, HAdd.hAdd and 5 more
Proof uses: CategoryTheory.CategoryStruct.comp, TopModuleCat.coker, HomologicalComplex.X, ComplexShape.up, TopRep.homogeneousCochains, HSub.hSub, OfNat.ofNat, TopModuleCat.ker, HomologicalComplex.d, ContinuousCohomology.bdryKer, CategoryTheory.Iso.hom, ContinuousCohomology.cohomologyIsoQuot, TopModuleCat.cokerDescBilinear, ContinuousCohomology.cupKerHom, ContinuousCohomology.continuous_cupKerCLM_uncurry, TopModuleCat.toModuleCat, ContinuousCohomology.cokerπ_cupKerCLM_bdryKer_left, ContinuousCohomology.cokerπ_cupKerCLM_bdryKer_right, TopModuleCat.linHomMap, CategoryTheory.Iso.inv
87 instances, coercions and auxiliary constants left out.
```
noncomputable def cup (f : ρ1 →ⁱL ρ2.linHom ρ3) (hp : Continuous fun p : M1 × M2 ↦ f p.1 p.2)
    (m n r : ℕ) (hr : r = m + n) :
    (continuousCohomology m (of ρ1)) ⟶
      TopModuleCat.linHom ((continuousCohomology n (of ρ2)))
        ((continuousCohomology r (of ρ3))) :=
…
```
Mentions: TopModuleCat.linHom