Chapter 6. Group Homology and Cohomology
FC05 — Weibel, An Introduction to Homological Algebra.
This chapter contains 31 definitions, 20 theorems, 5 propositions, 15 lemmas, 15 corollaries, 37 examples, 17 constructions, 1 remark, 2 conventions and 11 other statements.
Of the 154 statements checked against Lean, 53 are formalized somewhere and 101 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 101 | 66% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 42 | 27% | Mathlib states and proves it. |
| in another Lean project | 11 | 7% | Some other Lean development has it; using it means porting that code. |
| checked in total | 154 |
- Project-first search was performed at repo HEAD
f90173886bc881c2d43c0a7eb2d9fe7f110ac9a5. No project declaration owns a complete C06 source row under strict bundle semantics. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0 and directly project-compatible. EveryProw target was inspected at this revision. - Current Mathlib was refreshed on 2026-09-06 at
H=5aedf732b6987e8c26ab3c9ebc855314f82b045f. H-only declarations are not treated as project-compatible without an independently justified import route. The H audit did not close the remaining strict C06 bundles. C=ccc3323c6750abca25b49b35106f54eb3a398509isgit@github.com:kbuzzard/ClassFieldTheory.git, Apache-2.0, Lean 4.33.0-rc1. Its exact augmentation-ideal, regular-invariants, and cyclic Tate declarations are cited on U007, U011 and U021. These arereference-port, notpackage-import, because the audited toolchain differs from the project Lean 4.33.0 pin.T=167a73f2577fa7a600ee7977e0db599f12d92389isgit@github.com:TauCetiProject/TauCeti.git, Apache-2.0, Lean 4.34.0-rc2. Its fixed-action/factor-set/H² extension declarations own U065 and U067–U072; its smooth-discrete coefficient interface owns U141. All arereference-portfor the same toolchain reason.- TauCeti’s profinite continuous-cohomology development is not blanket coverage.
TauCeti/RepresentationTheory/Homological/ContCohomology/FiniteQuotient.leanexplicitly constructs the finite-quotient system while stating that the colimit theorem identifying it with continuous cohomology is not supplied there. Its low-degree files likewise do not supply the source’s full H² classification of profinite extensions. U143–U150 therefore stay unmatched unless the complete source bundle exists. - P/H make
A^HandA_HintoG/H-representations, but the audit found no checked adjunction with quotient restriction matching all of U098. The pinned low-degree inflation/restriction exactness is not substituted for the full LHS five-term sequences U100 without an LHS spectral sequence. - Pinned
Rep.barResolutionowns the unnormalized bar differential and resulting (co)homology computations. It does not supply Weibel’s normalized quotient in which a symbol containing1vanishes. U048, U050, U052 and U056 are therefore not over-credited, while U049, U051 and U053–U055 receive their exact P routes. - U121 is matched by
ProperlyDiscontinuousSMultogether withContinuousConstSMuland freeness viaIsCancelSMul: the neighborhood theorem gives disjointness for translates not fixing the base point, and freeness converts that tog ≠ 1. Nis dated 2026-09-06 negative evidence after project-first inspection, P, H/current Mathlib, the exact C/T revisions above, relevant open/current/indexed searches already recorded in the audit session, and broad Lean-source searches. A prerequisite, low-degree shadow, or one clause of a bundled statement is not credited as a route for the whole row.
Definition — Left G-module and G-mod
For a group G, a left G-module is an abelian group A with an action of G by additive automorphisms. G-mod identifies with left ZG-modules and with functors from the one-object category G to Ab.
Formalized. Mathlib/RepresentationTheory/Rep/Basic.lean::Rep.repIsoAction; Mathlib/RepresentationTheory/Rep/Iso.lean::Rep.equivalenceModuleMonoidAlgebra — At k=ℤ, Rep ℤ G is equivalent both to categorical G-actions and to modules over ℤ[G], matching the source presentations of left G-modules.
Searched: P
Definition — Trivial G-module, invariants, and coinvariants
The exact trivial-module functor Ab→G-mod sends A to the zero-action module. For a G-module A, A^G consists of fixed points and A_G=A/⟨ga-a⟩ is the coinvariant quotient.
Formalized. Mathlib/RepresentationTheory/Rep/Basic.lean::Rep.trivialFunctor; Mathlib/RepresentationTheory/Invariants.lean::Rep.invariantsFunctor, Rep.invariantsAdjunction; Mathlib/RepresentationTheory/Coinvariants.lean::Rep.coinvariantsFunctor, Rep.coinvariantsAdjunction — Pinned Mathlib packages the trivial representation and the fixed-point/coinvariant constructions as functors with the source universal properties.
Searched: P
Lemma 6.1.1 — Invariants and coinvariants as Hom/tensor
For the trivial G-module Z, A_G≅Z⊗_{ZG}A and A^G≅Hom_G(Z,A).
Formalized. Mathlib/RepresentationTheory/Invariants.lean::Rep.invariantsAdjunction; Mathlib/RepresentationTheory/Coinvariants.lean::Rep.coinvariantsTensor, Rep.coinvariantsAdjunction — At the trivial ℤ-representation these identify Hom_G(ℤ,A) with invariants and ℤ ⊗_{ℤ[G]} A with coinvariants.
Searched: P
Definition 6.1.2 — Group homology and cohomology
Define H_(G;A)=L_(-*G)(A)≅Tor**^{ZG}(Z,A) and H(G;A)=R^(-G)(A)≅Ext^*_{ZG}(Z,A); H_0=A_G and H0=AG.
Formalized. Mathlib/RepresentationTheory/Homological/GroupHomology/Basic.lean::groupHomologyIsoTor; Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean::groupCohomologyIsoExt — These are the source derived coinvariant/invariant definitions, expressed as Tor and Ext against the trivial representation.
Searched: P
Example 6.1.3 — Trivial group
For G=1 the invariant and coinvariant functors are the identity, so H_n(1;A)=H^n(1;A)=0 for n>0.
Formalized. Mathlib/RepresentationTheory/Homological/GroupHomology/Basic.lean::isZero_groupHomology_succ_of_subsingleton; Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean::isZero_groupCohomology_succ_of_subsingleton — For a subsingleton group all positive group homology and cohomology objects vanish, exactly the source calculation.
Searched: P
Example 6.1.4 — Infinite cyclic group
For T=⟨t⟩≅Z, the resolution 0→ZT→^{t-1}ZT→Z→0 computes H_0(T;A)=A/(t-1)A, H_1(T;A)=A^T, H0(T;A)=AT, H^1(T;A)=A/(t-1)A, with higher groups zero.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For T=⟨t⟩≅Z, the resolution 0→ZT→^{t-1}ZT→Z→0 computes H_0(T;A)=A/(t-1)A, H_1(T;A)=A^T, H0(T;A)=AT, H^1(T;A)=A/(t-1)A, with higher groups zero. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition 6.1.5 — Augmentation ideal
The augmentation ε:ZG→Z sends Σn_g g to Σn_g; its kernel I is the augmentation ideal, generated as an abelian group by g-1.
Formalized. ClassFieldTheory/Cohomology/AugmentationModule.lean::Rep.aug; Rep.aug.ι; Rep.aug.aug_shortExactSequence; Rep.aug.aug_isShortExact — The reference defines the augmentation module as the kernel of ε : R[G] → R and proves 0→aug→R[G]→R→0; at R=ℤ this is the source augmentation ideal.
Searched: C
Example 6.1.6 — Coinvariants via the augmentation ideal
Since Z≅ZG/I, H_0(G;A)=A_G≅A/IA; in particular H_0(G;Z)=Z.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: Since Z≅ZG/I, H_0(G;A)=A_G≅A/IA; in particular H_0(G;Z)=Z. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Example 6.1.7 — Regular module coefficients
Because ZG is projective over itself, H_n(G;ZG)=0 for n>0 and H_0(G;ZG)=Z; for finite G the corresponding positive-degree cohomology vanishing follows from Shapiro later.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: Because ZG is projective over itself, H_n(G;ZG)=0 for n>0 and H_0(G;ZG)=Z; for finite G the corresponding positive-degree cohomology vanishing follows from Shapiro later. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition 6.1.8 — Norm element
For finite G, N=Σ_{g∈G}g∈ZG is central and G-invariant.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For finite G, N=Σ_{g∈G}g∈ZG is central and G-invariant. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Lemma 6.1.9 — Invariants of the regular module
For finite G, (ZG)^G is the two-sided ideal Z·N generated by the norm.
Formalized. ClassFieldTheory/Cohomology/LeftRegular.lean::Rep.leftRegular.norm'; Rep.leftRegular.span_norm' — For finite G, the reference constructs the group-sum norm in the invariants of the regular representation and proves its span is all invariants; at R=ℤ this is (ℤG)^G=ℤ·N.
Searched: C
Proposition 6.1.10 — Vanishing when |G| is invertible
If |G|=m acts invertibly on A, e=N/m is a central idempotent and A_G≅A^G≅eA; all H_n(G;A),H^n(G;A) vanish for n>0.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: If |G|=m acts invertibly on A, e=N/m is a central idempotent and A_G≅A^G≅eA; all H_n(G;A),H^n(G;A) vanish for n>0. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Theorem 6.1.11 — H1 and abelianization
For every group G, H_1(G;Z)≅I/I^2≅G/[G,G].
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For every group G, H_1(G;Z)≅I/I^2≅G/[G,G]. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Theorem 6.1.12 — Trivial-coefficient universal coefficient formulas
For a trivial G-module A, H_1(G;A)≅G_ab⊗A, and in higher degrees the universal coefficient theorem expresses H_n(G;A) and H^n(G;A) from H_*(G;Z), tensor, Tor, and Ext over Z.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For a trivial G-module A, H_1(G;A)≅G_ab⊗A, and in higher degrees the universal coefficient theorem expresses H_n(G;A) and H^n(G;A) from H_*(G;Z), tensor, Tor, and Ext over Z. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Proposition 6.1.13 — Homology of a product of groups
For groups G,H, the Künneth theorem gives the natural split short exact sequence expressing H_n(G×H;Z) by tensor products and Tor_1 of H_(G;Z),H_(H;Z).
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For groups G,H, the Künneth theorem gives the natural split short exact sequence expressing H_n(G×H;Z) by tensor products and Tor_1 of H_(G;Z),H_(H;Z). Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Construction 6.1.14 — Cohomological cross product
Projective resolutions for G and H induce a natural cross product Hp(G;Z)⊗Hq(H;Z)→H^{p+q}(G×H;Z), compatible with tensor-product total complexes.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: Projective resolutions for G and H induce a natural cross product Hp(G;Z)⊗Hq(H;Z)→H^{p+q}(G×H;Z), compatible with tensor-product total complexes. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition 6.1.15 — Group hyperhomology and hypercohomology
For a chain complex of G-modules A_, write 𝕳_i(G;A_) for the hyper-derived functors of coinvariants; dually 𝕳i(G;A*) denotes hypercohomology of invariants.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For a chain complex of G-modules A_, write 𝕳_i(G;A_) for the hyper-derived functors of coinvariants; dually 𝕳i(G;A*) denotes hypercohomology of invariants. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Construction 6.2.1 — Periodic resolution of a cyclic group
For C_m=⟨σ⟩, (σ-1)N=N(σ-1)=0 and the alternating maps σ-1,N give a 2-periodic free ZC_m-resolution of Z.
Formalized. Mathlib/RepresentationTheory/Homological/FiniteCyclic.lean::Rep.FiniteCyclicGroup.resolution — Pinned Mathlib gives the finite-cyclic projective resolution with alternating generator-minus-one and norm maps, exactly the source 2-periodic resolution.
Searched: P
Theorem 6.2.2 — Homology and cohomology of a cyclic group
Applying tensor or Hom to the periodic resolution gives the standard 2-periodic formulas: odd/even positive degrees alternate between invariants modulo norms and norm-kernel modulo (σ-1), with the cohomological parity reversed accordingly.
Formalized. Mathlib/RepresentationTheory/Homological/GroupHomology/FiniteCyclic.lean::Rep.FiniteCyclicGroup.groupHomologyIsoEven, groupHomologyIsoOdd; Mathlib/RepresentationTheory/Homological/GroupCohomology/FiniteCyclic.lean::Rep.FiniteCyclicGroup.groupCohomologyIsoEven, groupCohomologyIsoOdd — The pinned even/odd isomorphisms identify cyclic group (co)homology with the norm and generator-minus-one kernels/quotients in the source parity.
Searched: P
Example 6.2.3 — Cyclic group with trivial integer coefficients
For C_m with trivial Z coefficients, H_{2i+1}(C_m;Z)≅Z/m, H_{2i}(C_m;Z)=0 for i>0, while H^{2i}(C_m;Z)≅Z/m for i>0 and odd cohomology vanishes.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For C_m with trivial Z coefficients, H_{2i+1}(C_m;Z)≅Z/m, H_{2i}(C_m;Z)=0 for i>0, while H^{2i}(C_m;Z)≅Z/m for i>0 and odd cohomology vanishes. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition 6.2.4 — Tate cohomology for cyclic groups
Extend cyclic cohomology to all integer degrees by hat H{2i}(C_m;A)=AG/NA and hat H^{2i+1}(C_m;A)=ker N/(σ-1)A.
Formalized. ClassFieldTheory/Cohomology/FiniteCyclic/ExplicitTate.lean::Representation.tateH0LinearEquiv, Representation.tateHNeg1LinearEquiv; ClassFieldTheory/Cohomology/FiniteCyclic/UpDown.lean::TateCohomology.periodicTateCohomology — The reference identifies degrees 0,-1 with invariants modulo norm and norm-kernel modulo generator-minus-one and transports them to every integer degree by period two.
Searched: C
Example 6.2.5 — Dimension shifting for Tate cohomology
A short exact sequence 0→K→P→A→0 with P projective yields hat H^n(G;A)≅hat H^{n+1}(G;K), since Tate cohomology of projectives vanishes.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: A short exact sequence 0→K→P→A→0 with P projective yields hat H^n(G;A)≅hat H^{n+1}(G;K), since Tate cohomology of projectives vanishes. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Proposition 6.2.6 — Augmentation ideal of a free group
If G is free on X, its augmentation ideal I⊂ZG is a free ZG-module with basis {x-1:x∈X}.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: If G is free on X, its augmentation ideal I⊂ZG is a free ZG-module with basis {x-1:x∈X}. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Corollary 6.2.7 — Cohomological dimension of a free group
For a free group G, 0→I→ZG→Z→0 is a free resolution, so H_n(G;A)=H^n(G;A)=0 for n≥2 and pd_{ZG}Z=1.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For a free group G, 0→I→ZG→Z→0 is a free resolution, so H_n(G;A)=H^n(G;A)=0 for n≥2 and pd_{ZG}Z=1. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Construction 6.2.8 — Free product of groups
The free product G*H is the coproduct of groups; every nonidentity element has a unique reduced alternating word in nonidentity elements of G and H.
Formalized. Mathlib/GroupTheory/CoprodI.lean::Monoid.CoprodI; Monoid.CoprodI.lift; Monoid.CoprodI.Word; Monoid.CoprodI.Word.equiv — For groups, CoprodI is the categorical free product and Word.equiv supplies the unique reduced alternating normal form required by the source.
Searched: P
Proposition 6.2.9 — Augmentation ideal of a free product
For Λ=Z(GH), I_{GH}≅(I_G⊗{ZG}Λ)⊕(I_H⊗{ZH}Λ) as Λ-modules.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For Λ=Z(GH), I_{GH}≅(I_G⊗{ZG}Λ)⊕(I_H⊗{ZH}Λ) as Λ-modules. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Corollary 6.2.10 — Higher (co)homology of a free product
For any (GH)-module A and n≥2, H_n(GH;A)≅H_n(G;A)⊕H_n(H;A), and similarly for cohomology.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For any (GH)-module A and n≥2, H_n(GH;A)≅H_n(G;A)⊕H_n(H;A), and similarly for cohomology. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition 6.3.1 — Induced and coinduced modules
For H≤G and an H-module A, Ind_H^G A=ZG⊗_{ZH}A and Coind_H^G A=Hom_H(ZG,A), with their natural G-actions.
Formalized. Mathlib/RepresentationTheory/Induced.lean::Rep.ind; Mathlib/RepresentationTheory/Coinduced.lean::Rep.coind — The pinned functors implement induction by group-algebra tensor and coinduction by equivariant Hom/functions with their natural G-actions.
Searched: P
Theorem 6.3.2 — Shapiro’s lemma
For H≤G, H_(G;Ind_H^G A)≅H_(H;A) and H^(G;Coind_H^G A)≅H^(H;A).
Formalized. Mathlib/RepresentationTheory/Homological/GroupHomology/Shapiro.lean::groupHomology.indIso; Mathlib/RepresentationTheory/Homological/GroupCohomology/Shapiro.lean::groupCohomology.coindIso — These natural isomorphisms are exactly Shapiro for homology of induced modules and cohomology of coinduced modules.
Searched: P
Corollary 6.3.3 — Shapiro for the trivial subgroup
For an abelian group A, induced/coinduced modules from H=1 have group (co)homology A in degree zero and vanish in positive degrees.
Formalized. Mathlib/RepresentationTheory/Homological/GroupHomology/Shapiro.lean::groupHomology.indIso; Mathlib/RepresentationTheory/Homological/GroupCohomology/Shapiro.lean::groupCohomology.coindIso; Mathlib/RepresentationTheory/Homological/GroupHomology/Basic.lean::isZero_groupHomology_succ_of_subsingleton; Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean::isZero_groupCohomology_succ_of_subsingleton — Specializing the pinned Shapiro isomorphisms to the trivial subgroup gives the coefficient module in degree zero and the pinned subsingleton-group vanishing in positive degrees.
Searched: P
Lemma 6.3.4 — Induction equals coinduction at finite index
If [G:H]<∞, Ind_H^G A≅Coind_H^G A naturally.
Formalized. Mathlib/RepresentationTheory/FiniteIndex.lean::Rep.indCoindIso; Rep.indCoindNatIso — For finite index, pinned Mathlib gives the natural isomorphism between induced and coinduced representations required by the source.
Searched: P
Corollary 6.3.5 — Finite-group cohomology of induced modules
For finite G, H^n(G;ZG⊗_Z A)=0 for n>0.
Formalized. Mathlib/RepresentationTheory/FiniteIndex.lean::Rep.indCoindIso; Mathlib/RepresentationTheory/Homological/GroupCohomology/Shapiro.lean::groupCohomology.coindIso; Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean::isZero_groupCohomology_succ_of_subsingleton — For the trivial subgroup of a finite group, induction is coinduction and Shapiro reduces positive cohomology to the trivial-group vanishing theorem.
Searched: P
Corollary 6.3.6 — Tate cohomology of projectives
For finite G and projective G-module P, hat H^n(G;P)=0 in every integer degree.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For finite G and projective G-module P, hat H^n(G;P)=0 in every integer degree. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Theorem 6.3.7 — Additive form of Hilbert 90
For a finite Galois extension L/K with group G, L^G≅L_G≅K and H_n(G;L)=H^n(G;L)=0 for n>0.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For a finite Galois extension L/K with group G, L^G≅L_G≅K and H_n(G;L)=H^n(G;L)=0 for n>0. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Example 6.3.8 — Cyclic additive Hilbert 90
For cyclic L/K with generator σ, the periodic cyclic calculation identifies trace with the norm element and gives exactness of the alternating σ-1 and trace maps on L.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For cyclic L/K with generator σ, the periodic cyclic calculation identifies trace with the norm element and gives exactness of the alternating σ-1 and trace maps on L. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Example 6.3.9 — Transfer at finite index
For H≤G of finite index, the natural map from a G-module A into Coind_H^G A≅Ind_H^G A induces transfer/corestriction maps in (co)homology; on degree zero these are the coset-sum/norm maps.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For H≤G of finite index, the natural map from a G-module A into Coind_H^G A≅Ind_H^G A induces transfer/corestriction maps in (co)homology; on degree zero these are the coset-sum/norm maps. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition 6.4.1 — Derivation / crossed homomorphism
A derivation D:G→A into a left G-module satisfies D(gh)=gD(h)+D(g); derivations form an abelian group Der(G,A).
Formalized. Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean::groupCohomology.IsCocycle₁; groupCohomology.cocycles₁ — The degree-one cocycle equation is exactly D(gh)=g·D(h)+D(g), and the cocycles form the source additive group of derivations.
Searched: P
Example 6.4.2 — Principal derivations
Each a∈A defines D_a(g)=ga-a; these form the subgroup PDer(G,A)⊂Der(G,A).
Formalized. Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean::groupCohomology.IsCoboundary₁; groupCohomology.coboundaries₁ — Degree-one coboundaries are precisely maps g ↦ g·a-a, so the pinned subgroup is the source principal derivations.
Searched: P
Example 6.4.3 — Derivations from augmentation-ideal maps
A G-map φ:I→A determines D_φ(g)=φ(g-1), a derivation.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: A G-map φ:I→A determines D_φ(g)=φ(g-1), a derivation. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Lemma 6.4.4 — Augmentation ideal represents derivations
The map φ↦D_φ is a natural isomorphism Hom_G(I,A)≅Der(G,A).
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: The map φ↦D_φ is a natural isomorphism Hom_G(I,A)≅Der(G,A). Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Theorem 6.4.5 — H^1 as derivations modulo principal derivations
There is a natural isomorphism H^1(G;A)≅Der(G,A)/PDer(G,A).
Formalized. Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean::groupCohomology.H1; groupCohomology.H1π; groupCohomology.cocycles₁; groupCohomology.coboundaries₁ — Pinned Mathlib realizes H¹ as the quotient of degree-one cocycles by coboundaries, hence derivations modulo principal derivations.
Searched: P
Corollary 6.4.6 — H^1 with trivial coefficients
If A is trivial, H^1(G;A)≅Der(G,A)≅Hom_Grp(G,A), equivalently Hom(G_ab,A).
Formalized. Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean::groupCohomology.H1IsoOfIsTrivial — For trivial action, pinned Mathlib identifies H¹(G,A) with additive homomorphisms from the abelianized group, exactly the source specialization.
Searched: P
Theorem 6.4.7 — Multiplicative Hilbert 90
For a finite Galois extension L/K with group G, the G-module L^× satisfies H1(G;L×)=0.
Formalized. Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean::groupCohomology.H1ofAutOnUnitsUnique; isMulCoboundary₁_of_isMulCocycle₁_of_aut_to_units — The pinned Hilbert-90 file proves multiplicative 1-cocycles for the Galois action on units are coboundaries, equivalently H¹(G,Lˣ)=0.
Searched: P
Example 6.4.8 — Cyclic multiplicative Hilbert 90
For cyclic L/K, H1(G;L×)=0 says every norm-one element has the form σ(b)/b; the degree-zero Tate quotient records K×/N_{L/K}(L×).
Formalized. Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean::exists_div_of_norm_eq_one — For a cyclic Galois action, the pinned theorem gives the source norm-one representation a=σ(b)/b.
Searched: P
Construction — Semidirect product A⋊G
For a G-module A, A×G becomes a group with (a,g)(b,h)=(a+gb,gh); this semidirect product is a split extension of G by A.
Formalized. Mathlib/GroupTheory/SemidirectProduct.lean::SemidirectProduct; SemidirectProduct.inl; SemidirectProduct.inr; SemidirectProduct.lift — The pinned multiplication is the source A⋊G multiplication, and the canonical maps exhibit it as the corresponding split extension.
Searched: P
Definition 6.4.9 — Stabilizing automorphism of a semidirect product
An automorphism of A⋊G stabilizes A and G when it fixes A pointwise and induces the identity on the quotient G.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: An automorphism of A⋊G stabilizes A and G when it fixes A pointwise and induces the identity on the quotient G. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Example 6.4.10 — Dihedral groups
Let C_2 act on C_m by inversion. Then C_m⋊C_2 is the dihedral group D_m; the corresponding H^1 calculation measures stabilizing automorphisms via derivations modulo principal ones.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: Let C_2 act on C_m by inversion. Then C_m⋊C_2 is the dihedral group D_m; the corresponding H^1 calculation measures stabilizing automorphisms via derivations modulo principal ones. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Construction — Normalized and unnormalized bar resolutions
Define canonical free ZG-resolutions B_* and B_*^u of the trivial module Z, with basis symbols [g_1|…|g_n] (normalized symbols omit entries equal to 1).
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: Define canonical free ZG-resolutions B_* and B_*^u of the trivial module Z, with basis symbols [g_1|…|g_n] (normalized symbols omit entries equal to 1). Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition 6.5.1 — Bar differential
On B_n^u, d=Σ_{i=0}n(-1)i d_i, where d_0 uses the G-action on the first entry, interior faces multiply adjacent group elements, and d_n drops the final entry.
Formalized. Mathlib/RepresentationTheory/Homological/Resolution.lean::Rep.barComplex.d, Rep.barComplex.d_single — The pinned differential is the source alternating inhomogeneous bar formula: action first face, adjacent-products interior faces, and final deletion face.
Searched: P
Convention — Normalized bar symbols with an identity entry vanish
In the normalized bar complex, [g_1|…|g_n] is taken to be zero whenever some g_i=1; this makes the differential formulas uniform.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: In the normalized bar complex, [g_1|…|g_n] is taken to be zero whenever some g_i=1; this makes the differential formulas uniform. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Examples 6.5.2 — Low bar differentials
The bar differential gives d[g]=(g-1)[ ], d[g|h]=g[h]-[gh]+[g], and the analogous alternating formula in degree three; its degree-one image is the augmentation ideal.
Formalized. Mathlib/RepresentationTheory/Homological/Resolution.lean::Rep.barComplex.d_single; Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean::groupCohomology.d₀₁, groupCohomology.d₁₂ — Specializing the pinned bar differential in low degrees yields the displayed source formulas and the ordinary degree-zero/one coboundaries.
Searched: P
Theorem 6.5.3 — Exactness of the bar resolutions
Both normalized and unnormalized bar complexes are exact augmented complexes of free ZG-modules, hence free resolutions of Z.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: Both normalized and unnormalized bar complexes are exact augmented complexes of free ZG-modules, hence free resolutions of Z. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Example 6.5.4 — Homology from the bar resolution
For a right G-module A, H_(G;A) is the homology of A⊗{ZG}B** (and analogously for left modules using the mirrored resolution).
Formalized. Mathlib/RepresentationTheory/Homological/Resolution.lean::Rep.barResolution; Mathlib/RepresentationTheory/Homological/GroupHomology/Basic.lean::groupHomology.inhomogeneousChains, groupHomology.inhomogeneousChainsIso — The pinned projective bar resolution yields the inhomogeneous chain complex computing H_*(G;A) as in the source.
Searched: P
Example 6.5.5 — Cohomology from bar cochains
For a left G-module A, H^(G;A) is the cohomology of Hom_G(B_,A); n-cochains identify with normalized functions G^n→A and the coboundary is the standard inhomogeneous group-cochain formula.
Formalized. Mathlib/RepresentationTheory/Homological/Resolution.lean::Rep.barResolution; Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean::groupCohomology.inhomogeneousCochains, groupCohomology.inhomogeneousCochainsIso — Applying Hom to the pinned bar resolution gives the inhomogeneous cochain complex with the standard source differential.
Searched: P
Example 6.5.6 — Low-dimensional bar cohomology
Degree-zero cocycles are A^G; one-coboundaries are principal derivations and one-cocycles are derivations, recovering H^1(G;A)=Der/PDer.
Formalized. Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean::groupCohomology.H0Iso; groupCohomology.cocycles₁; groupCohomology.coboundaries₁; groupCohomology.H1 — Degree zero is invariants and degree one is cocycles modulo coboundaries, i.e. derivations modulo principal derivations, exactly the source calculation.
Searched: P
Example 6.5.7 — Normalized 2-cocycles
A normalized 2-cochain ψ:G×G→A is a 2-cocycle exactly when ψ(1,g)=ψ(g,1)=0 and gψ(h,k)-ψ(gh,k)+ψ(g,hk)-ψ(g,h)=0; coboundaries have the corresponding δ of a 1-cochain.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: A normalized 2-cochain ψ:G×G→A is a 2-cocycle exactly when ψ(1,g)=ψ(g,1)=0 and gψ(h,k)-ψ(gh,k)+ψ(g,hk)-ψ(g,h)=0; coboundaries have the corresponding δ of a 1-cochain. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Theorem 6.5.8 — Finite-group torsion bound
If |G|=m, then for every G-module A and n>0, both H_n(G;A) and H^n(G;A) are annihilated by m.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: If |G|=m, then for every G-module A and n>0, both H_n(G;A) and H^n(G;A) are annihilated by m. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Corollary 6.5.9 — Vanishing after inverting |G|
If |G| acts invertibly on A (e.g. A is a Q-vector space or Z[1/m]-module), all positive-degree group homology and cohomology vanish.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: If |G| acts invertibly on A (e.g. A is a Q-vector space or Z[1/m]-module), all positive-degree group homology and cohomology vanish. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Corollary 6.5.10 — Finiteness for finitely generated coefficients
For finite G and finitely generated G-module A, H_n(G;A) and H^n(G;A) are finite abelian groups for n>0.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For finite G and finitely generated G-module A, H_n(G;A) and H^n(G;A) are finite abelian groups for n>0. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Shuffle Product 6.5.11 — Product on the bar complex
For abelian G, define the shuffle product of normalized bar symbols by summing signed (p,q)-shuffles; it is compatible with the bar differential and gives the bar complex a graded product.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For abelian G, define the shuffle product of normalized bar symbols by summing signed (p,q)-shuffles; it is compatible with the bar differential and gives the bar complex a graded product. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Example 6.5.12 — Low shuffle products
For abelian G, the shuffle product begins [g]*[h]=[g|h]-[h|g] and extends by the signed shuffle rule.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For abelian G, the shuffle product begins [g]*[h]=[g|h]-[h|g] and extends by the signed shuffle rule. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Theorem 6.5.13 — Bar complex as a DGA
For abelian G, the normalized bar complex with shuffle product is a differential graded algebra.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For abelian G, the normalized bar complex with shuffle product is a differential graded algebra. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Corollary 6.5.14 — Ring structure on group homology
For abelian G and a commutative ZG-algebra R, H_*(G;R) inherits a graded-commutative ring structure from the shuffle product.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For abelian G and a commutative ZG-algebra R, H_*(G;R) inherits a graded-commutative ring structure from the shuffle product. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition 6.6.1 — Group extension and splitting
An extension of G by an abelian group A is a short exact sequence 0→A→E→G→1; conjugation in E induces a G-action on A. It splits when the projection has a group-homomorphic section, equivalently E is a semidirect product for the induced action.
Formalized. Mathlib/GroupTheory/GroupExtension/Defs.lean::GroupExtension; GroupExtension.Section; GroupExtension.Splitting — Pinned Mathlib bundles a short exact group extension, section, and homomorphic splitting; its API identifies split extensions with semidirect products.
Searched: P
Extension Problem 6.6.2 — Extensions inducing a fixed action
Fix a G-module A and ask for extensions 0→A→E→G→1 whose conjugation action on A is the prescribed G-action.
Formalized. TauCeti/GroupTheory/GroupExtension/FactorSetOfSection.lean::GroupExtension.InducesAction; GroupExtension.conjActOfSection — TauCeti records the action induced on the abelian kernel and the predicate that it equals a prescribed G-action, matching the source extension problem.
Searched: T
Definition — Equivalence of group extensions
Two extensions of G by A are equivalent when there is an isomorphism of middle groups inducing the identity on A and G.
Formalized. Mathlib/GroupTheory/GroupExtension/Defs.lean::GroupExtension.Equiv — The pinned equivalence is an isomorphism of middle groups commuting with the kernel inclusion and quotient map, matching equivalence of extensions with fixed ends.
Searched: P
Classification Theorem 6.6.3 — H^2 classifies group extensions
Equivalence classes of extensions of G by the fixed G-module A are in bijection with H^2(G;A).
Formalized. TauCeti/GroupTheory/GroupExtension/Cohomology.lean::GroupExtension.cohomologyClassEquiv; GroupExtension.exists_cohomologyClass_eq — TauCeti constructs the cohomology class and an equivalence between extension-equivalence classes and H², exactly the source classification theorem.
Searched: T
Definition 6.6.4 — Factor set
Given an extension and a based set-theoretic section σ:G→E, define the factor set [g,h]∈A by σ(g)σ(h)=[g,h]σ(gh).
Formalized. TauCeti/GroupTheory/GroupExtension/FactorSetOfSection.lean::GroupExtension.factorSetFun; GroupExtension.factorSet — Given a based section, TauCeti defines the kernel-valued factor satisfying the source multiplication equation and packages it as a normalized factor set.
Searched: T
Lemma 6.6.5 — Equal factor sets give equivalent extensions
Two extensions equipped with based sections that yield the same factor set are equivalent.
Formalized. TauCeti/GroupTheory/GroupExtension/FactorSetOfSection.lean::GroupExtension.factorSetToGroupExtensionEquiv; TauCeti/GroupTheory/GroupExtension/Cohomology.lean::GroupExtension.nonempty_equiv_iff_cohomologyClass_factorSet_eq — The constructed equivalence and criterion imply equal factor sets give equivalent extensions, exactly the source statement.
Searched: T
Corollary 6.6.6 — Zero factor set and split extensions
A zero factor set corresponds to a homomorphic section and hence a split extension; normalized factor sets are compared with normalized 2-cocycles.
Formalized. TauCeti/GroupTheory/GroupExtension/Of/FactorSet.lean::FactorSet.trivialSplitting; TauCeti/GroupTheory/GroupExtension/Cohomology.lean::GroupExtension.nonempty_splitting_iff_cohomologyClass_eq_zero — The trivial factor set has its canonical splitting, and TauCeti proves splitting exists iff the extension class vanishes.
Searched: T
Theorem 6.6.7 — Factor sets are normalized 2-cocycles
A function G×G→A occurs as a factor set exactly when it is a normalized 2-cocycle in the bar complex.
Formalized. TauCeti/GroupTheory/GroupExtension/Of/FactorSet.lean::FactorSet.isMulCocycle₂, FactorSet.map_one_fst, FactorSet.map_one_snd; TauCeti/GroupTheory/GroupExtension/FactorSetOfSection.lean::GroupExtension.factorSet — TauCeti packages factor sets as normalized multiplicative 2-cocycles and proves the source unit-normalization identities.
Searched: T
Construction 6.6.8 — Changing a section changes by a coboundary
If two based sections of one extension differ by a normalized 1-cochain, their factor sets differ by its coboundary; hence an extension determines a well-defined class in H^2(G;A).
Formalized. TauCeti/GroupTheory/GroupExtension/FactorSetOfSection.lean::GroupExtension.sectionDiff; GroupExtension.isMulCoboundary₂_div — TauCeti proves that changing sections changes the factor set by a 2-coboundary, exactly the source section-change law.
Searched: T
Theorem 6.6.9 — Schur–Zassenhaus splitting in the coprime abelian-kernel case
If |G| and |A| are finite and coprime, every extension of G by A splits.
Formalized. Mathlib/GroupTheory/SchurZassenhaus.lean::Subgroup.exists_right_complement'_of_coprime; Subgroup.exists_left_complement'_of_coprime — Pinned Mathlib proves the stronger complement theorem for a finite normal subgroup of order coprime to its index; the source abelian-kernel splitting is a specialization.
Searched: P
Example 6.6.10 — Crossed-product algebras
For a finite Galois extension L/K with group G and a factor set in L^×, twist the multiplication on the L-module L[G] to obtain a crossed-product K-algebra; cohomologous factor sets give equivalent algebras.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For a finite Galois extension L/K with group G and a factor set in L^×, twist the multiplication on the L-module L[G] to obtain a crossed-product K-algebra; cohomologous factor sets give equivalent algebras. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition 6.6.11 — Relative Brauer group
For finite Galois L/K, Br(L/K) consists of Brauer classes of central simple K-algebras split by L; crossed products identify Br(L/K) with H2(G;L×).
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For finite Galois L/K, Br(L/K) consists of Brauer classes of central simple K-algebras split by L; crossed products identify Br(L/K) with H2(G;L×). Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Construction 6.6.12 — H^3 from four-term extensions
From an exact sequence 0→A→N→E→G→1 with A central in N, choices of section and lifts produce a normalized 3-cocycle; this motivates the crossed-module interpretation of H^3.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: From an exact sequence 0→A→N→E→G→1 with A central in N, choices of section and lifts produce a normalized 3-cocycle; this motivates the crossed-module interpretation of H^3. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition — Crossed module
A crossed module is a homomorphism α:N→E together with an E-action on N satisfying α(m)·n=mnm^{-1} and α(e·n)=eα(n)e^{-1}.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: A crossed module is a homomorphism α:N→E together with an E-action on N satisfying α(m)·n=mnm^{-1} and α(e·n)=eα(n)e^{-1}. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition — Equivalence of crossed modules and the H^3 class
Crossed modules with kernel A and cokernel G are related by elementary equivalences preserving A and G; the 3-cocycle construction gives an invariant H^3(G;A)-class under the generated equivalence relation.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: Crossed modules with kernel A and cokernel G are related by elementary equivalences preserving A and G; the 3-cocycle construction gives an invariant H^3(G;A)-class under the generated equivalence relation. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Theorem 6.6.13 — H^3 classifies crossed modules
Equivalence classes of crossed modules with kernel A and cokernel G are in bijection with H^3(G;A).
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: Equivalence classes of crossed modules with kernel A and cokernel G are in bijection with H^3(G;A). Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition 6.7.1 — Restriction and corestriction for a group map
A homomorphism ρ:H→G induces exact restriction of modules ρ^#. The natural maps on coinvariants and invariants extend to corestriction H_(H;ρ^#A)→H_(G;A) and restriction H(G;A)→H^(H;ρ#A).
Formalized. Mathlib/RepresentationTheory/Homological/GroupCohomology/Functoriality.lean::groupCohomology.map, groupCohomology.resNatTrans; Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean::groupHomology.map, groupHomology.coresNatTrans — Pinned functoriality supplies contravariant restriction in cohomology and covariant corestriction in homology for group maps with compatible coefficients.
Searched: P
Construction 6.7.2 — Subgroup restriction/corestriction on resolutions
For H≤G, ZG is free as a ZH-module, so projective G-resolutions restrict to projective H-resolutions and realize restriction/corestriction explicitly at chain level.
Formalized. Mathlib/RepresentationTheory/Rep/Res.lean::Rep.resFunctor; Mathlib/RepresentationTheory/Coinduced.lean::Rep.resCoindAdjunction; Mathlib/RepresentationTheory/Homological/GroupCohomology/Functoriality.lean::groupCohomology.resNatTrans; Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean::groupHomology.coresNatTrans — Restriction along a subgroup inclusion and the pinned resolution functoriality realize the source subgroup restriction/corestriction construction.
Searched: P
Construction 6.7.3 — Inflation and coinflation
For H normal in G, the quotient map G→G/H and the maps A→A_H, A^H→A define inflation in cohomology and coinflation in homology between G/H and G.
Formalized. Mathlib/RepresentationTheory/Invariants.lean::Rep.quotientToInvariantsFunctor; Mathlib/RepresentationTheory/Coinvariants.lean::Rep.quotientToCoinvariantsFunctor; Mathlib/RepresentationTheory/Homological/GroupCohomology/Functoriality.lean::groupCohomology.infNatTrans; Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean::groupHomology.coinfNatTrans — Pinned Mathlib forms quotient-group invariant/coinvariant coefficients and the resulting inflation/coinflation maps exactly as in the source.
Searched: P
Example 6.7.4 — Inflation/corestriction for trivial H-action
When H acts trivially on A, inflation agrees with the corresponding restriction construction and coinflation with corestriction; for cyclic quotient maps this recovers the natural maps between the periodic computations.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: When H acts trivially on A, inflation agrees with the corresponding restriction construction and coinflation with corestriction; for cyclic quotient maps this recovers the natural maps between the periodic computations. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Construction 6.7.5 — Covariant category of group-module pairs
Let C have objects (G,A) and morphisms (H,B)→(G,A) given by ρ:H→G and an H-map B→ρ^#A. Group homology is functorial covariantly in these pairs.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: Let C have objects (G,A) and morphisms (H,B)→(G,A) given by ρ:H→G and an H-map B→ρ^#A. Group homology is functorial covariantly in these pairs. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Construction 6.7.6 — Contravariant category of group-module pairs
Let D have the same objects but a morphism (H,B)→(G,A) consists of ρ:H→G and an H-map ρ^#A→B. Group cohomology is contravariantly functorial through restriction followed by the coefficient map.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: Let D have the same objects but a morphism (H,B)→(G,A) consists of ρ:H→G and an H-map ρ^#A→B. Group cohomology is contravariantly functorial through restriction followed by the coefficient map. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Example 6.7.7 — Conjugation maps
For H≤G and g∈G, conjugation identifies H with gHg^{-1}; multiplication by g on a G-module gives the compatible coefficient map and hence natural conjugation maps on group (co)homology.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For H≤G and g∈G, conjugation identifies H with gHg^{-1}; multiplication by g on a G-module gives the compatible coefficient map and hence natural conjugation maps on group (co)homology. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Theorem 6.7.8 — Inner automorphisms act trivially
Conjugation by any g∈G induces the identity on H_(G;Z) and H^(G;Z).
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: Conjugation by any g∈G induces the identity on H_(G;Z) and H^(G;Z). Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Corollary 6.7.9 — Quotient action for a normal subgroup
If H is normal in G, conjugation gives a well-defined G/H-action on H_(H;Z) and H^(H;Z), since conjugation by elements of H acts trivially.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: If H is normal in G, conjugation gives a well-defined G/H-action on H_(H;Z) and H^(H;Z), since conjugation by elements of H acts trivially. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Example 6.7.10 — Conjugation on cyclic (co)homology in a dihedral group
For C_m normal in D_m with quotient C_2 acting by σ↦σ^{-1}, conjugation acts by (-1)^i on H_{2i-1}(C_m;Z) and H^{2i}(C_m;Z).
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For C_m normal in D_m with quotient C_2 acting by σ↦σ^{-1}, conjugation acts by (-1)^i on H_{2i-1}(C_m;Z) and H^{2i}(C_m;Z). Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Construction — Cup product by diagonal restriction
Compose the cohomological cross product with restriction along Δ:G→G×G to define x∪y=Δ^(x×y) in H^(G;Z).
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: Compose the cohomological cross product with restriction along Δ:G→G×G to define x∪y=Δ^(x×y) in H^(G;Z). Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Theorem 6.7.11 — Cohomology ring
The cup product makes H^*(G;Z) an associative graded-commutative unital ring, naturally in G.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: The cup product makes H^*(G;Z) an associative graded-commutative unital ring, naturally in G. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Lemma 6.7.12 — Graded symmetry of the cross product
Under the transposition τ:G×H→H×G, τ^*(y×x)=(-1)^{pq}x×y for x∈H^p(G;Z), y∈H^q(H;Z).
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: Under the transposition τ:G×H→H×G, τ^*(y×x)=(-1)^{pq}x×y for x∈H^p(G;Z), y∈H^q(H;Z). Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Construction 6.7.13 — Coalgebra
A coalgebra over a commutative ring k is a k-module H with coassociative coproduct Δ:H→H⊗H and counit ε:H→k satisfying the counit identities; cocommutativity means τΔ=Δ.
Formalized. Mathlib/RingTheory/Coalgebra/Basic.lean::CoalgebraStruct; Coalgebra; Coalgebra.IsCocomm — Pinned Mathlib bundles coproduct/counit with coassociativity and counit laws, plus the source cocommutativity condition.
Searched: P
Lemma 6.7.14 — Coalgebra structure on group homology
If k is a field, or H_(G;k) is flat over k, the diagonal G→G×G and Künneth isomorphism make H_(G;k) a cocommutative coalgebra.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: If k is a field, or H_(G;k) is flat over k, the diagonal G→G×G and Künneth isomorphism make H_(G;k) a cocommutative coalgebra. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition 6.7.15 — Bialgebra and Hopf algebra
A bialgebra is an algebra whose coproduct and counit are algebra maps and make it a cocommutative coalgebra; a Hopf algebra also has an antipode satisfying the two convolution-inverse identities.
Formalized. Mathlib/RingTheory/Bialgebra/Basic.lean::Bialgebra; Mathlib/RingTheory/HopfAlgebra/Basic.lean::HopfAlgebra; Mathlib/RingTheory/Coalgebra/Basic.lean::Coalgebra.IsCocomm — Pinned Mathlib packages compatible algebra/coalgebra data and antipode identities; adding IsCocomm gives the source convention.
Searched: P
Construction 6.7.16 — Transfer
For a normal finite-index subgroup H≤G, summing over right cosets defines A_G→A_H and extends by universality to homological transfer H_(G;A)→H_(H;A); dually there is a cohomological transfer.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For a normal finite-index subgroup H≤G, summing over right cosets defines A_G→A_H and extends by universality to homological transfer H_(G;A)→H_(H;A); dually there is a cohomological transfer. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Lemma 6.7.17 — Transfer followed by corestriction/restriction
For finite-index H≤G, cor∘tr is multiplication by [G:H] on H_*(G;A), and the analogous transfer-restriction composite is multiplication by [G:H] in cohomology.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For finite-index H≤G, cor∘tr is multiplication by [G:H] on H_*(G;A), and the analogous transfer-restriction composite is multiplication by [G:H] in cohomology. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Lemma 6.8.1 — (Co)invariants for a normal subgroup
If H normal in G, A_H and A^H are naturally G/H-modules. Restriction from G/H-mod to G-mod has coinvariants by H as left adjoint and invariants by H as right adjoint.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: If H normal in G, A_H and A^H are naturally G/H-modules. Restriction from G/H-mod to G-mod has coinvariants by H as left adjoint and invariants by H as right adjoint. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Lyndon–Hochschild–Serre Spectral Sequence 6.8.2
For H normal in G there are convergent first-quadrant sequences E^2_{pq}=H_p(G/H;H_q(H;A))⇒H_{p+q}(G;A) and E_2{pq}=Hp(G/H;Hq(H;A))⇒H{p+q}(G;A).
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For H normal in G there are convergent first-quadrant sequences E^2_{pq}=H_p(G/H;H_q(H;A))⇒H_{p+q}(G;A) and E_2{pq}=Hp(G/H;Hq(H;A))⇒H{p+q}(G;A). Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Construction 6.8.3 — Low-degree LHS exact sequences
The homological and cohomological low-degree terms of the LHS spectral sequences give the standard five-term exact sequences involving (co)inflation, (co)restriction, and H_1/H_2 or H1/H2.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: The homological and cohomological low-degree terms of the LHS spectral sequences give the standard five-term exact sequences involving (co)inflation, (co)restriction, and H_1/H_2 or H1/H2. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Example 6.8.4 — Central subgroup calculation
When H lies in the center and coefficients are trivial, G/H acts trivially on H_(H;A),H^(H;A); the LHS E^2-page can then be computed from the homology of H and universal-coefficient formulas, as illustrated for C_m⊂C_{2m} with m odd.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: When H lies in the center and coefficients are trivial, G/H acts trivially on H_(H;A),H^(H;A); the LHS E^2-page can then be computed from the homology of H and universal-coefficient formulas, as illustrated for C_m⊂C_{2m} with m odd. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Example 6.8.5 — Dihedral groups via LHS
For C_m normal in D_{2m} with m odd, the quotient C_2 action from 6.7.10 determines the LHS page and yields the corresponding homology/cohomology pattern of the dihedral group.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For C_m normal in D_{2m} with m odd, the quotient C_2 action from 6.7.10 determines the LHS page and yields the corresponding homology/cohomology pattern of the dihedral group. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Example 6.8.6 — Gysin sequence for a central infinite cyclic subgroup
If central t∈G has infinite order and T=⟨t⟩, the LHS sequence for 1→T→G→G/T→1 collapses to the stated Gysin long exact sequence for trivial coefficients.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: If central t∈G has infinite order and T=⟨t⟩, the LHS sequence for 1→T→G→G/T→1 collapses to the stated Gysin long exact sequence for trivial coefficients. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Construction 6.8.7 — Free presentation and low-degree LHS sequence
A presentation G=F/R with F free gives 1→R→F→G→1. Since F and R have homological dimension one, the low-degree LHS sequence identifies the obstruction term controlling H_2(G;Z).
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: A presentation G=F/R with F free gives 1→R→F→G→1. Since F and R have homological dimension one, the low-degree LHS sequence identifies the obstruction term controlling H_2(G;Z). Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Hopf Formula 6.8.8
For a free presentation G=F/R, H_2(G;Z)≅(R∩[F,F])/[F,R].
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For a free presentation G=F/R, H_2(G;Z)≅(R∩[F,F])/[F,R]. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition — Central and universal central extensions of groups
A central extension 0→A→X→G→1 has A in Z(X). It is universal if there is a unique homomorphism over G from X to every central extension of G.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: A central extension 0→A→X→G→1 has A in Z(X). It is universal if there is a unique homomorphism over G from X to every central extension of G. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition — Perfect group
A group G is perfect when G=[G,G], equivalently G_ab=0.
Formalized. Mathlib/GroupTheory/IsPerfect.lean::Group.IsPerfect; Group.isPerfect_def; Group.IsPerfect.commutator_eq_top — Pinned Mathlib defines perfection by equality with the commutator subgroup, the primary source definition; abelianization-zero is the equivalent quotient formulation.
Searched: P
Example 6.9.1 — Binary icosahedral extension of A5
A_5 is perfect and PSL_2(F_5)≅A_5 is covered centrally by SL_2(F_5) with kernel {±I}; this is its universal central extension.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: A_5 is perfect and PSL_2(F_5)≅A_5 is covered centrally by SL_2(F_5) with kernel {±I}; this is its universal central extension. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Lemma 6.9.2 — Universality forces perfection
If G has a universal central extension X→G, then both G and X are perfect.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: If G has a universal central extension X→G, then both G and X are perfect. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Construction 6.9.3 — Central extension from a free presentation
For 1→R→F→G→1, quotienting by [R,F] gives a central extension R/[R,F]→F/[R,F]→G; if G is perfect, restricting to [F,F]/[R,F] remains surjective with kernel (R∩[F,F])/[R,F].
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For 1→R→F→G→1, quotienting by [R,F] gives a central extension R/[R,F]→F/[R,F]→G; if G is perfect, restricting to [F,F]/[R,F] remains surjective with kernel (R∩[F,F])/[R,F]. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Lemma 6.9.4 — The presentation cover is perfect
If G is perfect, [F,F]/[R,F] in Construction 6.9.3 is itself perfect.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: If G is perfect, [F,F]/[R,F] in Construction 6.9.3 is itself perfect. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Theorem 6.9.5 — Universal central extension theorem
A group has a universal central extension iff it is perfect. For a free presentation F/R, it is 0→H_2(G;Z)→[F,F]/[R,F]→G→1.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: A group has a universal central extension iff it is perfect. For a free presentation F/R, it is 0→H_2(G;Z)→[F,F]/[R,F]→G→1. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Lemma 6.9.6 — Uniqueness from a perfect source
If X→G and Y→G are central extensions and X is perfect, there is at most one homomorphism X→Y over G.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: If X→G and Y→G are central extensions and X is perfect, there is at most one homomorphism X→Y over G. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Recognition Theorem 6.9.7 — Universal central extensions
A central extension X→G is universal iff X is perfect and every central extension of X splits as a direct product X×A.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: A central extension X→G is universal iff X is perfect and every central extension of X splits as a direct product X×A. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Corollary 6.9.8 — Universal cover is superperfect in degrees one and two
If X→G is universal central, then H_1(X;Z)=H_2(X;Z)=0.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: If X→G is universal central, then H_1(X;Z)=H_2(X;Z)=0. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Corollary 6.9.9 — Vanishing Schur multiplier splits central extensions
If G is perfect and H_2(G;Z)=0, every central extension of G is a direct product with its abelian kernel.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: If G is perfect and H_2(G;Z)=0, every central extension of G is a direct product with its abelian kernel. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Example 6.9.10 — Alternating groups and Schur multipliers
For n≥5 the alternating groups are perfect; their H_2(A_n;Z) (Schur multipliers) determine the kernels of their universal central extensions, with the listed exceptional values for small n.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For n≥5 the alternating groups are perfect; their H_2(A_n;Z) (Schur multipliers) determine the kernels of their universal central extensions, with the listed exceptional values for small n. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Example 6.9.11 — Special linear groups
Except for the stated small finite-field cases, SL_n(F) is perfect. Its center is μ_n(F), so PSL_n(F) is a central quotient; universal-cover behavior is governed by H_2.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: Except for the stated small finite-field cases, SL_n(F) is perfect. Its center is μ_n(F), so PSL_n(F) is a central quotient; universal-cover behavior is governed by H_2. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Example 6.9.12 — Elementary matrix groups
For n≥3, the elementary subgroup E_n(R)⊂GL_n(R) generated by elementary matrices is perfect, using commutator identities among elementary matrices.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For n≥3, the elementary subgroup E_n(R)⊂GL_n(R) generated by elementary matrices is perfect, using commutator identities among elementary matrices. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition 6.9.13 — Steinberg group
For n≥3, St_n(R) is generated by x_{ij}^λ with the additive and Steinberg commutator relations mirroring elementary matrices; it maps naturally onto E_n(R).
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For n≥3, St_n(R) is generated by x_{ij}^λ with the additive and Steinberg commutator relations mirroring elementary matrices; it maps naturally onto E_n(R). Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition — Proper action used for covering spaces
A group action on a topological space X is proper here when every point has an open neighborhood U disjoint from each nontrivial translate gU; translations are assumed continuous.
Formalized. Mathlib/Topology/Algebra/ConstMulAction.lean::ProperlyDiscontinuousSMul.exists_nhds_disjoint_image; IsCancelSMul; ContinuousConstSMul — For a free continuous group action, the pinned properly-discontinuous neighborhood theorem gives a neighborhood disjoint from every nonidentity translate, exactly the source condition.
Searched: P
Example 6.10.1 — Universal-covering action
If Y is connected and locally simply connected, G=π_1(Y) acts properly by deck transformations on the universal cover X=Ỹ and X/G≅Y.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: If Y is connected and locally simply connected, G=π_1(Y) acts properly by deck transformations on the universal cover X=Ỹ and X/G≅Y. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Lemma 6.10.2 — Singular chains under a proper action
If G acts properly on X, the singular chain complex S_(X) is degreewise free over ZG and its coinvariant complex is naturally S_(X/G).
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: If G acts properly on X, the singular chain complex S_(X) is degreewise free over ZG and its coinvariant complex is naturally S_(X/G). Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Corollary 6.10.3 — G-action on singular (co)homology
A proper G-action on X induces G-module structures on H_(X;Z) and H^(X;Z).
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: A proper G-action on X induces G-module structures on H_(X;Z) and H^(X;Z). Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition 6.10.4 — Classifying space BG and universal space EG
A CW complex BG with π_1(BG)=G and contractible universal cover is a classifying space for G; its universal cover is denoted EG.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: A CW complex BG with π_1(BG)=G and contractible universal cover is a classifying space for G; its universal cover is denoted EG. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Theorem 6.10.5 — Group (co)homology equals (co)homology of BG
For any classifying space BG, H_(BG;Z)≅H_(G;Z) and H^(BG;Z)≅H^(G;Z).
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For any classifying space BG, H_(BG;Z)≅H_(G;Z) and H^(BG;Z)≅H^(G;Z). Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Example 6.10.6 — Models for BZ
S^1 and C^× are models for BZ; their universal covers R and C are contractible with quotient maps given by the standard exponential/translation coverings.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: S^1 and C^× are models for BZ; their universal covers R and C are contractible with quotient maps given by the standard exponential/translation coverings. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Example 6.10.7 — Model for BC2
S^∞ is contractible with the free antipodal C_2-action, so RP∞=S∞/C_2 is a model for BC_2.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: S^∞ is contractible with the free antipodal C_2-action, so RP∞=S∞/C_2 is a model for BC_2. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Example 6.10.8 — Aspherical Riemann surfaces
For an orientable surface S of genus g>0 with the standard one-relator presentation of π_1(S), its contractible universal cover makes S a model for Bπ_1(S).
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For an orientable surface S of genus g>0 with the standard one-relator presentation of π_1(S), its contractible universal cover makes S a model for Bπ_1(S). Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Example 6.10.9 — Locally symmetric classifying spaces
If L is connected with maximal compact K and Γ≤L is discrete torsion-free, X=L/K is contractible and Γ acts properly, so Γ∖X is a model for BΓ.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: If L is connected with maximal compact K and Γ≤L is discrete torsion-free, X=L/K is contractible and Γ acts properly, so Γ∖X is a model for BΓ. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Theorem 6.10.10 — Equivariant-to-quotient spectral sequences
If G acts properly on connected X and A is abelian, there are convergent spectral sequences H_p(G;H_q(X;A))⇒H_{p+q}(X/G;A) and Hp(G;Hq(X;A))⇒H^{p+q}(X/G;A).
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: If G acts properly on connected X and A is abelian, there are convergent spectral sequences H_p(G;H_q(X;A))⇒H_{p+q}(X/G;A) and Hp(G;Hq(X;A))⇒H^{p+q}(X/G;A). Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Krull Theorem 6.11.1 — Absolute Galois group as inverse limit
For a field K with separable closure K_s, Gal(K_s/K) is naturally the inverse limit of the finite Galois groups Gal(L/K) over finite Galois subextensions L/K.
Formalized. Mathlib/FieldTheory/Galois/Profinite.lean::InfiniteGalois.continuousMulEquivToLimit; InfiniteGalois.profiniteGalGrpIsoLimit — Pinned Mathlib identifies an infinite Galois group with the inverse limit over finite Galois subextensions; the source absolute Galois statement is the separable-closure specialization.
Searched: P
Example 6.11.2 — Absolute Galois group of a finite field
For F_q, finite subextensions are F_{q^n} ordered by divisibility and Gal(overline F_q/F_q) is the inverse limit of the cyclic groups Z/n, i.e. the profinite completion hat Z.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For F_q, finite subextensions are F_{q^n} ordered by divisibility and Gal(overline F_q/F_q) is the inverse limit of the cyclic groups Z/n, i.e. the profinite completion hat Z. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition — Profinite topology on an inverse limit
Give each finite set/group the discrete topology and an inverse limit the subspace topology from the product; this compact Hausdorff topology is the profinite topology.
Formalized. Mathlib/Topology/Category/Profinite/AsLimit.lean::Profinite.asLimitCone; Profinite.asLimitConeIso; Profinite.asLimit — Pinned Mathlib realizes a profinite object as the topological limit of finite discrete quotients, implementing the source inverse-limit topology intrinsically.
Searched: P
Definition 6.11.3 — Profinite set
A profinite set is an inverse limit of finite sets equipped with the profinite topology; the chosen presentation is not part of the data.
Formalized. Mathlib/Topology/Category/Profinite/Basic.lean::Profinite; Profinite.of; Mathlib/Topology/Category/Profinite/AsLimit.lean::Profinite.asLimit — Pinned Profinite bundles the topology rather than a chosen presentation, while asLimit proves the finite inverse-limit presentation, exactly matching the source notion.
Searched: P
Definition — Totally disconnected space
A topological space is totally disconnected when all connected components are singletons.
Formalized. Mathlib/Topology/Connected/Basic.lean::TotallyDisconnectedSpace — The pinned predicate states that connected components are singletons, exactly the source definition.
Searched: P
Theorem 6.11.4 — Characterization of profinite spaces
A space is profinite iff it is compact, Hausdorff, and totally disconnected. Hence the profinite structure depends only on the topology, not on a chosen inverse-limit presentation.
Formalized. Mathlib/Topology/Category/Profinite/Basic.lean::Profinite; Profinite.of; Mathlib/Topology/Category/Profinite/AsLimit.lean::Profinite.asLimit — Profinite is definitionally compact Hausdorff plus totally disconnected, Profinite.of constructs it from those hypotheses, and asLimit gives the inverse-limit direction.
Searched: P
Definition 6.11.5 — Profinite group
A profinite group is an inverse limit of finite groups with its profinite topology; equivalently it is a compact Hausdorff totally disconnected topological group.
Formalized. Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean::ProfiniteGrp — Pinned ProfiniteGrp is a profinite space with group and topological-group structures, exactly the source compact Hausdorff totally disconnected formulation.
Searched: P
Examples 6.11.6 — Profinite groups and completion
Finite groups, p-adic integers, and absolute Galois groups are profinite. The profinite completion of an abstract group is the inverse limit of its finite quotients.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: Finite groups, p-adic integers, and absolute Galois groups are profinite. The profinite completion of an abstract group is the inverse limit of its finite quotients. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Lemma 6.11.7 — Open normal subgroups recover a profinite group
For profinite G, open normal subgroups form a neighborhood basis of 1, every quotient G/U is finite, and the canonical map G→lim_U G/U is an isomorphism of profinite groups.
Formalized. Mathlib/Topology/Algebra/ClopenNhdofOne.lean::IsTopologicalGroup.exist_openNormalSubgroup_sub_open_nhds_of_one; Mathlib/Topology/Algebra/Category/ProfiniteGrp/Limits.lean::ProfiniteGrp.toFiniteQuotientFunctor, ProfiniteGrp.isoLimittoFiniteQuotientFunctor — Pinned Mathlib proves open normal subgroups refine neighborhoods of one and identifies a profinite group with the inverse limit of its finite quotients, matching the source lemma.
Searched: P
Definition 6.11.8 — Discrete module over a profinite group
A discrete G-module is a G-module A with A given the discrete topology such that G×A→A is continuous; equivalently each element has an open stabilizer.
Formalized. TauCeti/RepresentationTheory/Homological/ContCohomology/SmoothDiscrete.lean::TauCeti.IsSmoothDiscrete; TauCeti.isSmoothDiscrete_iff_continuousSMul; TauCeti.DiscreteRep; TauCeti/RepresentationTheory/Homological/ContCohomology/Discrete.lean::TauCeti.exists_openNormalSubgroup_smul_eq_self — TauCeti defines discrete coefficients by discrete topology plus open point stabilizers, proves equivalence with continuity, and refines stabilizers to open normal subgroups for profinite groups.
Searched: T
Examples 6.11.9 — Discrete Galois modules and finite groups
K_s is a discrete Gal(K_s/K)-module; if G is finite, every ordinary G-module is discrete.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: K_s is a discrete Gal(K_s/K)-module; if G is finite, every ordinary G-module is discrete. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Convention — Category CG of discrete G-modules
Let C_G be the full additive category of discrete G-modules with ordinary G-linear maps; it is an abelian subcategory of G-mod.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: Let C_G be the full additive category of discrete G-modules with ordinary G-linear maps; it is an abelian subcategory of G-mod. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Lemma 6.11.10 — Enough injectives for discrete profinite modules
The abelian category C_G of discrete G-modules has enough injective objects.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: The abelian category C_G of discrete G-modules has enough injective objects. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Remark — CG need not have enough projectives
In contrast with ordinary modules over a group ring, the category C_G of discrete profinite G-modules generally does not have enough projectives.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: In contrast with ordinary modules over a group ring, the category C_G of discrete profinite G-modules generally does not have enough projectives. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition 6.11.11 — Continuous cohomology of a profinite group
For profinite G and discrete G-module A, define H^*(G;A) as the right derived functors in C_G of invariants A↦A^G. For finite G this agrees with ordinary group cohomology.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For profinite G and discrete G-module A, define H^*(G;A) as the right derived functors in C_G of invariants A↦A^G. For finite G this agrees with ordinary group cohomology. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Definition 6.11.12 — Continuous cochains
For discrete A, C^n(G,A) is the abelian group of continuous maps G^n→A, with the usual inhomogeneous group-cochain differential.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For discrete A, C^n(G,A) is the abelian group of continuous maps G^n→A, with the usual inhomogeneous group-cochain differential. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Theorem 6.11.13 — Continuous cochain and finite-quotient formulas
For profinite G and discrete A, H(G;A)≅H^(C(G,A))≅colim_U H^(G/U;A^U), over open normal U.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For profinite G and discrete A, H(G;A)≅H^(C(G,A))≅colim_U H^(G/U;A^U), over open normal U. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Corollary 6.11.14 — Positive continuous cohomology is torsion
For n≥1 and discrete coefficients A, H^n(G;A) is a torsion abelian group.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For n≥1 and discrete coefficients A, H^n(G;A) is a torsion abelian group. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Low Dimensions 6.11.15 — Continuous H^1 and H^2
H^1(G;A) is continuous derivations modulo continuous principal derivations; H^2(G;A) consists of continuous factor-set classes and, for finite A, classifies profinite extensions of G by A.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: H^1(G;A) is continuous derivations modulo continuous principal derivations; H^2(G;A) consists of continuous factor-set classes and, for finite A, classifies profinite extensions of G by A. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Hilbert’s Theorem 90 6.11.16 — Absolute Galois cohomology
For G=Gal(K_s/K), K_s and K_s^× are discrete G-modules with invariants K and K^×; H^n(G;K_s)=0 for n>0 and H1(G;K_s×)=0, obtained as direct limits of finite Galois Hilbert-90 calculations.
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For G=Gal(K_s/K), K_s and K_s^× are discrete G-modules with invariants K and K^×; H^n(G;K_s)=0 for n>0 and H1(G;K_s×)=0, obtained as direct limits of finite Galois Hilbert-90 calculations. Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Brauer Group 6.11.17 — Brauer group as H^2
Br(K) is the group of Brauer classes of finite-dimensional central simple K-algebras (equivalently division-algebra classes). It is the union of Br(L/K), hence Br(K)≅H2(Gal(K_s/K);K_s×).
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: Br(K) is the group of Brauer classes of finite-dimensional central simple K-algebras (equivalently division-algebra classes). It is the union of Br(L/K), hence Br(K)≅H2(Gal(K_s/K);K_s×). Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Proposition 6.11.18 — Relative Brauer exact sequence
For a Galois extension L/K with group G, the low-degree Hochschild–Serre sequence gives 0→Br(L/K)→Br(K)→Br(L)G→H3(G;L×)→H3(K;K_s^×); in particular Br(L/K)=ker(Br(K)→Br(L)).
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: For a Galois extension L/K with group G, the low-degree Hochschild–Serre sequence gives 0→Br(L/K)→Br(K)→Br(L)G→H3(G;L×)→H3(K;K_s^×); in particular Br(L/K)=ker(Br(K)→Br(L)). Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.
Vista 6.11.19 — Standard Brauer-group comparisons
Records cohomological consequences including Tsen’s vanishing for one-variable function fields over algebraically closed fields, Br(R)≅Z/2, Br(K)≅Q/Z for local fields, and the global Hasse-invariant exact relation for Br(Q).
Not formalized. partial: adjacent group-(co)homology, group-theory, topology, or Galois infrastructure — No checked A/P/H/T/C declaration realizes the whole source bundle: Records cohomological consequences including Tsen’s vanishing for one-variable function fields over algebraically closed fields, Br(R)≅Z/2, Br(K)≅Q/Z for local fields, and the global Hasse-invariant exact relation for Br(Q). Under strict bundle semantics, adjacent prerequisites or a proper subset do not own the row.