Basic.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

20 declarations, 0 contain sorry, 0 declared as axioms

Complements on the coinduced resolutions computing continuous group cohomology

This file develops further API for the standard (coinduced) resolutions and the homogeneous cochain complexes computing continuous group cohomology.

Main definitions

ContRepresentation.resolutionCLM ρ2 ρ3 u i: the continuous linear map between objects of the underlying objects of the resolutions induced by a continuous linear map u : M2 →L[k] M3 where M2 and M3 are the underlying module of ρ2 and ρ3 respectively.
ContRepresentation.resolutionXCast X h: transport between two levels of the standard resolution along an equality of indices, as a continuous linear map.
ContRepresentation.invariantsObjIHom ρ2 ρ3 n r: the comparison morphism from the invariants of the internal hom of two levels of the coinduced resolutions to the internal hom of the corresponding homogeneous cochains.
ContinuousCohomology.bdryKer X j: the coboundary map into the kernel model, i.e. the differential corestricted to the cocycles of the next degree.
ContinuousCohomology.cohomologyIsoQuot X j: continuous cohomology identified with the quotient of the kernel model of the cocycles by the coboundaries, carrying the quotient topology.

Material destined for Mathlib.RepresentationTheory.Homological.ContCohomology.Basic.

Imports (5)

Imported by 2 files

def ContRepresentation.resolutionCLM Documented declaration: resolutionCLM line 64 source
Source documentation
The functorial extension of a continuous linear map u : M2 →L[k] M3 (not necessarily equivariant) to the i-th level of the standard resolutions, applying u pointwise under the iterated C(G, ·).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContinuousLinearMap, RingHom.id, Nat, TopRep.resolutionX, TopRep.of
46 instances, coercions and auxiliary constants left out.
```
def resolutionCLM (u : M2 →L[k] M3) :
    (i : ℕ) → resolutionX (of ρ2) i →L[k] resolutionX (of ρ3) i
  | 0 => u
  | i + 1 => (resolutionCLM u i).compLeftContinuous k G

@[simp]
```
lemma ContRepresentation.resolutionCLM_zero_apply line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContinuousLinearMap, RingHom.id, Eq, TopRep.resolutionX, TopRep.of, OfNat.ofNat, Nat, ContRepresentation.resolutionCLM
Proof uses: rfl
50 instances, coercions and auxiliary constants left out.
lemma ContRepresentation.resolutionCLM_succ_apply line 74 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContinuousLinearMap, RingHom.id, Nat, TopRep.resolutionX, TopRep.of, HAdd.hAdd, OfNat.ofNat, Eq, ContRepresentation.resolutionCLM
Proof uses: rfl
56 instances, coercions and auxiliary constants left out.
lemma ContRepresentation.resolutionCLM_add line 78 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContinuousLinearMap, RingHom.id, Nat, Eq, TopRep.resolutionX, TopRep.of, ContRepresentation.resolutionCLM, HAdd.hAdd
Proof uses: Nat.recAux, Eq.refl, OfNat.ofNat, ContinuousLinearMap.ext, ContinuousMap.ext, id, ContinuousMap, congrArg
57 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ContRepresentation.resolutionCLM_smul line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContinuousLinearMap, RingHom.id, Nat, Eq, TopRep.resolutionX, TopRep.of, ContRepresentation.resolutionCLM, HSMul.hSMul
Proof uses: Nat.recAux, Eq.refl, OfNat.ofNat, ContinuousLinearMap.ext, HAdd.hAdd, ContinuousMap.ext, id, ContinuousMap, congrArg
68 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ContRepresentation.resolutionCLM_conj Conjugating u : M2 →L[k] M3 by the representations corresponds to conjugating resolutionCLM u by the coinduced actions on the resolutions line 92 source
Source documentation
Conjugating u : M2 →L[k] M3 by the representations corresponds to conjugating resolutionCLM u by the coinduced actions on the resolutions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContinuousLinearMap, RingHom.id, Nat, Eq, TopRep.resolutionX, TopRep.of, ContRepresentation.resolutionCLM, ContinuousLinearMap.comp, Inv.inv, TopRep.ρ
Proof uses: Nat.recAux, Eq.refl, OfNat.ofNat, ContinuousLinearMap.ext, HAdd.hAdd, ContinuousMap.ext, id, ContinuousMap, Eq.mpr, HMul.hMul, congrArg, inv_inv, mul_inv_cancel_left
74 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma resolutionCLM_conj (h : G) (u : M2 →L[k] M3) (i : ℕ) :
    resolutionCLM ρ2 ρ3 (ρ3 h ∘L u ∘L ρ2 h⁻¹) i =
      (resolutionX (of ρ3) i).ρ h ∘L resolutionCLM ρ2 ρ3 u i ∘L
        (resolutionX (of ρ2) i).ρ h⁻¹ := by
…
```
Mentions: ContRepresentation.resolutionCLM
def ContRepresentation.resolutionXCast Transport between two levels of the standard resolution along an equality of indices, as a continuous linear map line 108 source
Source documentation
Transport between two levels of the standard resolution along an equality of indices, as a continuous linear map.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, IsTopologicalGroup, TopRep, Nat, Eq, ContinuousLinearMap, RingHom.id, TopRep.resolutionX
Proof uses: Eq.rec, ContinuousLinearMap.id
22 instances, coercions and auxiliary constants left out.
```
def resolutionXCast (X : TopRep k G) {i j : ℕ} (h : i = j) :
    ↥(resolutionX X i) →L[k] ↥(resolutionX X j) :=
…
```
lemma ContRepresentation.resolutionXCast_apply line 112 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, IsTopologicalGroup, TopRep, Nat, Eq, HAdd.hAdd, OfNat.ofNat, TopRep.resolutionX, ContinuousLinearMap, RingHom.id, ContRepresentation.resolutionXCast
Proof uses: Eq.refl
38 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ContRepresentation.resolutionXCast_trans line 118 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, IsTopologicalGroup, TopRep, Nat, Eq, TopRep.resolutionX, ContinuousLinearMap, RingHom.id, ContRepresentation.resolutionXCast, Eq.trans
Proof uses: Eq.rec, Eq.refl
26 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma ContRepresentation.d_hom_resolutionXCast line 123 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, IsTopologicalGroup, TopRep, Nat, Eq, TopRep.resolutionX, HAdd.hAdd, OfNat.ofNat, ContIntertwiningMap, TopRep.ρ, TopRep.Hom.hom, TopRep.d, ContinuousLinearMap, RingHom.id, ContRepresentation.resolutionXCast
Proof uses: Eq.rec, Eq.refl
38 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma ContRepresentation.d_hom_zero The zeroth differential of the standard resolution is the constant-function embedding line 129 source
Source documentation
The zeroth differential of the standard resolution is the constant-function embedding.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, IsTopologicalGroup, TopRep, Eq, TopRep.resolutionX, HAdd.hAdd, Nat, OfNat.ofNat, ContIntertwiningMap, TopRep.ρ, TopRep.Hom.hom, TopRep.d, ContinuousMap.const
Proof uses: rfl
26 instances, coercions and auxiliary constants left out.
```
lemma d_hom_zero (X : TopRep k G) (v : ↥X) :
    (d X 0).hom v = ContinuousMap.const G v := rfl
```
lemma ContRepresentation.d_hom_succ_apply The pointwise formula for the differentials of the standard resolution line 133 source
Source documentation
The pointwise formula for the differentials of the standard resolution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, IsTopologicalGroup, TopRep, Nat, TopRep.resolutionX, HAdd.hAdd, OfNat.ofNat, Eq, ContIntertwiningMap, TopRep.ρ, TopRep.Hom.hom, TopRep.d, HSub.hSub
Proof uses: rfl
34 instances, coercions and auxiliary constants left out.
```
lemma d_hom_succ_apply (X : TopRep k G) (i : ℕ) (F : ↥(resolutionX X (i + 1))) (x : G) :
    (d X (i + 1)).hom F x = F - (d X i).hom (F x) := rfl
```
lemma ContRepresentation.resolutionCLM_comp_d The differentials of the standard resolutions are compatible with the functorial extension resolutionCLM of a continuous linear map line 138 source
Source documentation
The differentials of the standard resolutions are compatible with the functorial extension resolutionCLM of a continuous linear map.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, ContinuousLinearMap, RingHom.id, Nat, TopRep.resolutionX, TopRep.of, Eq, HAdd.hAdd, OfNat.ofNat, ContIntertwiningMap, TopRep.ρ, TopRep.Hom.hom and 2 more
Proof uses: Nat.recAux, Eq.refl, ContinuousMap.ext, Trans.trans, HSub.hSub, Eq.mpr, id, congrArg, ContRepresentation.d_hom_succ_apply, ContRepresentation.resolutionCLM_succ_apply, Eq.symm, map_sub, RingHom
77 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma resolutionCLM_comp_d (u : M2 →L[k] M3) (i : ℕ) (y : ↥(resolutionX (of ρ2) i)) :
    (d (of ρ3) i).hom (resolutionCLM ρ2 ρ3 u i y) =
      resolutionCLM ρ2 ρ3 u (i + 1) ((d (of ρ2) i).hom y) := by
…
```
Mentions: ContRepresentation.resolutionCLM
abbrev ContRepresentation.invariantsObjIHom Documented declaration: invariantsObjIHom line 158 source
Source documentation
The comparison morphism from the invariants of the internal hom of two levels of the coinduced resolutions to the internal hom of the corresponding homogeneous cochains, restricting an equivariant continuous linear map to the invariants on both sides.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, Nat, Quiver.Hom, TopModuleCat, CategoryTheory.Functor.obj, TopRep, TopRep.invariantsFunctor, TopRep.iHom, HomologicalComplex.X, ComplexShape.up, TopRep.resolution', TopRep.of and 2 more
Proof uses: TopModuleCat.ofHom, Subtype, Membership.mem, Submodule, ContRepresentation.invariants, TopRep.ρ, ContinuousLinearMap, RingHom.id, TopModuleCat.toModuleCat, ContinuousLinearMap.mk, LinearMap.mk, AddHom.mk, ContRepresentation.invariantsObjIHom.match_1, ContinuousLinearMap.restrict
98 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
abbrev invariantsObjIHom (n r : ℕ) : (invariantsFunctor k G).obj
    (((of ρ2).resolution'.X n).iHom ((of ρ3).resolution'.X r)) ⟶
    ((of ρ2).homogeneousCochains.X n).linHom ((of ρ3).homogeneousCochains.X r) :=
…
```
Mentions: ContRepresentation.linHom
lemma ContRepresentation.eqToHom_iHom_apply Applying an eqToHom reindexing morphism between internal homs of resolution levels to elements is transport along the index equality line 184 source
Source documentation
Applying an eqToHom reindexing morphism between internal homs of resolution levels to elements is transport along the index equality.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, AddCommGroup, Module, IsTopologicalAddGroup, ContinuousSMul, IsTopologicalGroup, ContRepresentation, TopRep, Nat, Eq, TopRep.iHom, TopRep.resolutionX, TopRep.of, RingHom.id, ContIntertwiningMap, TopRep.ρ, CategoryTheory.ConcreteCategory.hom, CategoryTheory.eqToHom and 2 more
Proof uses: Eq.rec, Eq.refl
58 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma eqToHom_iHom_apply (A : TopRep k G) {i j : ℕ} (h : i = j)
    (pf : A.iHom (resolutionX (.of ρ3) i) = A.iHom (resolutionX (.of ρ3) j))
    (Φ : ↥(A.iHom (resolutionX (.of ρ3) i))) (τ : ↥A) :
    (eqToHom pf) Φ τ = resolutionXCast (.of ρ3) h (Φ τ) := by
…
```
Mentions: ContRepresentation.resolutionXCast
lemma ContinuousCohomology._root_.TopRep.homogeneousCochains.d_comp_d_apply Applying two consecutive differentials of the homogeneous cochain complex gives zero line 204 source
Source documentation
Applying two consecutive differentials of the homogeneous cochain complex gives zero.
```
lemma _root_.TopRep.homogeneousCochains.d_comp_d_apply (X : TopRep k G) (i j l : ℕ)
    (σ : (homogeneousCochains X).X i) :
    (homogeneousCochains X).d j l ((homogeneousCochains X).d i j σ) = 0 := by
…
```
def ContinuousCohomology.bdryKer The coboundary map into the kernel model: the differential corestricted to the cocycles of the next degree line 212 source
Source documentation
The coboundary map into the kernel model: the differential corestricted to the cocycles of the next degree. In degree 0 the junk value d 0 0 = 0 makes its range ⊥, matching the convention of HomologicalComplex.homologyIsCokernel.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, IsTopologicalGroup, TopRep, Nat, Quiver.Hom, TopModuleCat, HomologicalComplex.X, ComplexShape.up, TopRep.homogeneousCochains, HSub.hSub, OfNat.ofNat, TopModuleCat.ker, HAdd.hAdd, HomologicalComplex.d
Proof uses: TopModuleCat.ofHom, Subtype, TopRep.resolution', Membership.mem, Submodule, ContRepresentation.invariants, TopRep.ρ, TopModuleCat.toModuleCat, LinearMap.ker, RingHom.id, TopModuleCat.Hom.hom, ContinuousLinearMap.codRestrict
67 instances, coercions and auxiliary constants left out.
```
noncomputable def bdryKer (X : TopRep k G) (j : ℕ) :
    (homogeneousCochains X).X (j - 1) ⟶
      TopModuleCat.ker ((homogeneousCochains X).d j (j + 1)) :=
…
```
lemma ContinuousCohomology.bdryKer_apply_coe line 219 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, IsTopologicalGroup, TopRep, Nat, TopModuleCat.toModuleCat, HomologicalComplex.X, TopModuleCat, ComplexShape.up, TopRep.homogeneousCochains, HSub.hSub, OfNat.ofNat, Eq, Membership.mem, Submodule, LinearMap.ker, HAdd.hAdd, RingHom.id, TopModuleCat.Hom.hom and 5 more
Proof uses: rfl
66 instances, coercions and auxiliary constants left out.
lemma ContinuousCohomology.toCycles_comp_cyclesIsoKer_hom Under the identification of the cycles with the kernel model, toCycles becomes the corestricted differential bdryKer line 224 source
Source documentation
Under the identification of the cycles with the kernel model, toCycles becomes the corestricted differential bdryKer.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, IsTopologicalGroup, TopRep, Nat, Eq, Quiver.Hom, TopModuleCat, HomologicalComplex.X, ComplexShape.up, TopRep.homogeneousCochains, HSub.hSub, OfNat.ofNat, TopModuleCat.ker, HAdd.hAdd, HomologicalComplex.d, CategoryTheory.CategoryStruct.comp, HomologicalComplex.cycles, HomologicalComplex.sc and 4 more
Proof uses: CategoryTheory.ConcreteCategory.hom_ext, ContinuousLinearMap, RingHom.id, TopModuleCat.toModuleCat, Subtype.ext, Membership.mem, Submodule, LinearMap.ker, TopModuleCat.Hom.hom, CategoryTheory.ConcreteCategory.hom, Eq.mpr, id, congrArg, CategoryTheory.ConcreteCategory.comp_apply, HomologicalComplex.iCycles, HomologicalComplex.cyclesIsoKer_hom_apply_coe, ContinuousCohomology.bdryKer_apply_coe, HomologicalComplex.toCycles_i
62 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma toCycles_comp_cyclesIsoKer_hom (X : TopRep k G) (j : ℕ) :
    (homogeneousCochains X).toCycles (j - 1) j ≫
      ((homogeneousCochains X).cyclesIsoKer j (j + 1) (by simp)).hom = bdryKer X j := by
…
```
Mentions: ContinuousCohomology.bdryKer
def ContinuousCohomology.cohomologyIsoQuot Continuous cohomology identified with the quotient of the kernel model of the cocycles by the coboundaries, carrying the quotient topology line 234 source
Source documentation
Continuous cohomology identified with the quotient of the kernel model of the cocycles by the coboundaries, carrying the quotient topology.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Group, IsTopologicalGroup, TopRep, Nat, CategoryTheory.Iso, TopModuleCat, continuousCohomology, TopModuleCat.coker, HomologicalComplex.X, ComplexShape.up, TopRep.homogeneousCochains, HSub.hSub, OfNat.ofNat, TopModuleCat.ker, HAdd.hAdd, HomologicalComplex.d, ContinuousCohomology.bdryKer
Proof uses: CategoryTheory.Iso.trans, HomologicalComplex.cycles, HomologicalComplex.toCycles, HomologicalComplex.homologyIsoCoker, CochainComplex.prev_nat, TopModuleCat.cokerCongr, HomologicalComplex.cyclesIsoKer, ContinuousCohomology.toCycles_comp_cyclesIsoKer_hom
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
noncomputable def cohomologyIsoQuot (X : TopRep k G) (j : ℕ) :
    continuousCohomology j X ≅ TopModuleCat.coker (bdryKer X j) :=
…
```
Mentions: ContinuousCohomology.bdryKer