Invariants descended along lifts to refinements

Let φ : A → A' be an equivariant map between the coefficient modules of two formations F and F' on G, and let σ assign to every finite normal layer L a homomorphism σ_L : H²(L, A) → ℚ/ℤ that does not change under inflation to a refinement of L. Suppose that

• every class of H²(L, A') becomes, after inflation to some refinement L' of L, the image under φ of a class of H²(L', A), and
• σ vanishes on the classes that φ kills.

Then σ descends to an invariant descendedInv φ σ … L : H²(L, A') → ℚ/ℤ on every layer: the invariant of a class is σ of a lift of an inflation of it, whichever refinement and lift are chosen (descendedInv_eq). It is characterized by the two equations descendedInv_map (on the image of φ it is σ) and descendedInv_infl (it does not change under inflation) (descendedInv_unique). This is the shape of Tate's definition of the invariant map of idele classes from the sum of the local invariants of ideles. That sum is defined on H²(L, I_L) and, because it vanishes on the kernel of H²(L, I_L) → H²(L, C_L), induces an invariant only on the image of this map, which can be a proper subgroup: for the biquadratic field ℚ(√13, √17) the image is killed by 2 while H²(L, C_L) is cyclic of order 4. Classically, every class lifts after inflation to a suitable cyclotomic refinement.

The invariant inherits the restriction and conjugation laws of σ (descendedInv_res, descendedInv_conj), because restriction, conjugation and the maps induced by φ commute with inflation. Suppose moreover that H¹ of every layer of F' vanishes, that σ vanishes exactly on the classes that φ kills, and that every layer L, of degree n, has a refinement carrying a class with σ = 1/n. Then the invariant of L is injective with image the n-torsion of ℚ/ℤ, and F' is a class formation with this invariant (ClassFormation.ofDescendedInv). Injectivity holds because inflation is injective once H¹ vanishes. The image of a class with σ = 1/n on a refinement L' restricts to zero on the layer L'/L, where σ becomes n • (1/n) = 0, so by the inflation-restriction sequence it is inflated from L.

Main definitions

• TauCeti.ClassFieldTheory.descendedInv: the invariant of F' descended from σ.
• TauCeti.ClassFieldTheory.ClassFormation.ofDescendedInv: the class formation on F' with the descended invariant.

Main statements

• TauCeti.ClassFieldTheory.descendedInv_eq: the invariant of a class is σ of any lift of any inflation of it.
• TauCeti.ClassFieldTheory.descendedInv_map, TauCeti.ClassFieldTheory.descendedInv_infl and TauCeti.ClassFieldTheory.descendedInv_unique: the two equations that characterize it.
• TauCeti.ClassFieldTheory.descendedInv_res, TauCeti.ClassFieldTheory.descendedInv_conj: its restriction and conjugation laws.
• TauCeti.ClassFieldTheory.descendedInv_injective, TauCeti.ClassFieldTheory.range_descendedInv: its injectivity and its image.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VIII, §4.
• J. Tate, Global class field theory, in J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter VII, §11.

The descended invariant

noncomputable def TauCeti.ClassFieldTheory.descendedInv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} (φ : F.toRep ⟶ F'.toRep) (σ : (L : NormalLayer G) → ↑(L.H F 2) →+ AddCircle 1) (hσ : ∀ {old new : NormalLayer G} (T : LayerRefinement old new) (y : ↑(old.H F 2)), (σ new) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F 2)) y) = (σ old) y) (hlift : ∀ (L : NormalLayer G) (x : ↑(L.H F' 2)), ∃ (L' : NormalLayer G) (T : LayerRefinement L L') (y : ↑(L'.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L'.Gal) (L'.repMap φ) 2)) y = (CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F' 2)) x) (hker : ∀ (L : NormalLayer G) (y : ↑(L.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = 0 → (σ L) y = 0) (L : NormalLayer G) : ↑(L.H F' 2) →+ AddCircle 1

The invariant of F' descended from σ: the invariant of a class of H²(L, A') is the value of σ on a lift, along φ, of its inflation to some refinement of L. By descendedInv_eq it does not depend on the refinement or on the lift.

theorem TauCeti.ClassFieldTheory.descendedInv_eq {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} (φ : F.toRep ⟶ F'.toRep) (σ : (L : NormalLayer G) → ↑(L.H F 2) →+ AddCircle 1) (hσ : ∀ {old new : NormalLayer G} (T : LayerRefinement old new) (y : ↑(old.H F 2)), (σ new) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F 2)) y) = (σ old) y) (hlift : ∀ (L : NormalLayer G) (x : ↑(L.H F' 2)), ∃ (L' : NormalLayer G) (T : LayerRefinement L L') (y : ↑(L'.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L'.Gal) (L'.repMap φ) 2)) y = (CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F' 2)) x) (hker : ∀ (L : NormalLayer G) (y : ↑(L.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = 0 → (σ L) y = 0) {L L' : NormalLayer G} (T : LayerRefinement L L') {x : ↑(L.H F' 2)} {y : ↑(L'.H F 2)} (h : (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L'.Gal) (L'.repMap φ) 2)) y = (CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F' 2)) x) : (descendedInv φ σ ⋯ hlift hker L) x = (σ L') y

The invariant of a class is σ of any lift of any inflation of it: if the inflation of x to a refinement L' of L is the image under φ of y, then the descended invariant of x is σ_{L'} y.

@[simp]

theorem TauCeti.ClassFieldTheory.descendedInv_map {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} (φ : F.toRep ⟶ F'.toRep) (σ : (L : NormalLayer G) → ↑(L.H F 2) →+ AddCircle 1) (hσ : ∀ {old new : NormalLayer G} (T : LayerRefinement old new) (y : ↑(old.H F 2)), (σ new) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F 2)) y) = (σ old) y) (hlift : ∀ (L : NormalLayer G) (x : ↑(L.H F' 2)), ∃ (L' : NormalLayer G) (T : LayerRefinement L L') (y : ↑(L'.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L'.Gal) (L'.repMap φ) 2)) y = (CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F' 2)) x) (hker : ∀ (L : NormalLayer G) (y : ↑(L.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = 0 → (σ L) y = 0) {L : NormalLayer G} (y : ↑(L.H F 2)) : (descendedInv φ σ ⋯ hlift hker L) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y) = (σ L) y

On the image of φ the descended invariant is σ.

@[simp]

theorem TauCeti.ClassFieldTheory.descendedInv_infl {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} (φ : F.toRep ⟶ F'.toRep) (σ : (L : NormalLayer G) → ↑(L.H F 2) →+ AddCircle 1) (hσ : ∀ {old new : NormalLayer G} (T : LayerRefinement old new) (y : ↑(old.H F 2)), (σ new) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F 2)) y) = (σ old) y) (hlift : ∀ (L : NormalLayer G) (x : ↑(L.H F' 2)), ∃ (L' : NormalLayer G) (T : LayerRefinement L L') (y : ↑(L'.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L'.Gal) (L'.repMap φ) 2)) y = (CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F' 2)) x) (hker : ∀ (L : NormalLayer G) (y : ↑(L.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = 0 → (σ L) y = 0) {old new : NormalLayer G} (T : LayerRefinement old new) (x : ↑(old.H F' 2)) : (descendedInv φ σ ⋯ hlift hker new) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F' 2)) x) = (descendedInv φ σ ⋯ hlift hker old) x

The descended invariant does not change under inflation.

theorem TauCeti.ClassFieldTheory.descendedInv_unique {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} (φ : F.toRep ⟶ F'.toRep) (σ : (L : NormalLayer G) → ↑(L.H F 2) →+ AddCircle 1) (hσ : ∀ {old new : NormalLayer G} (T : LayerRefinement old new) (y : ↑(old.H F 2)), (σ new) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F 2)) y) = (σ old) y) (hlift : ∀ (L : NormalLayer G) (x : ↑(L.H F' 2)), ∃ (L' : NormalLayer G) (T : LayerRefinement L L') (y : ↑(L'.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L'.Gal) (L'.repMap φ) 2)) y = (CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F' 2)) x) (hker : ∀ (L : NormalLayer G) (y : ↑(L.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = 0 → (σ L) y = 0) (inv : (L : NormalLayer G) → ↑(L.H F' 2) →+ AddCircle 1) (hmap : ∀ (L : NormalLayer G) (y : ↑(L.H F 2)), (inv L) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y) = (σ L) y) (hinfl : ∀ {old new : NormalLayer G} (T : LayerRefinement old new) (x : ↑(old.H F' 2)), (inv new) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F' 2)) x) = (inv old) x) : inv = descendedInv φ σ ⋯ hlift hker

The descended invariant is determined by its two equations: a family of homomorphisms H²(L, A') → ℚ/ℤ that agrees with σ on the image of φ and does not change under inflation is the descended invariant.

@[simp]

theorem TauCeti.ClassFieldTheory.descendedInv_res {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} (φ : F.toRep ⟶ F'.toRep) (σ : (L : NormalLayer G) → ↑(L.H F 2) →+ AddCircle 1) (hσ : ∀ {old new : NormalLayer G} (T : LayerRefinement old new) (y : ↑(old.H F 2)), (σ new) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F 2)) y) = (σ old) y) (hlift : ∀ (L : NormalLayer G) (x : ↑(L.H F' 2)), ∃ (L' : NormalLayer G) (T : LayerRefinement L L') (y : ↑(L'.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L'.Gal) (L'.repMap φ) 2)) y = (CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F' 2)) x) (hker : ∀ (L : NormalLayer G) (y : ↑(L.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = 0 → (σ L) y = 0) (hres : ∀ {small big : NormalLayer G} (R : LayerRestriction small big) (y : ↑(big.H F 2)), (σ small) ((CategoryTheory.ConcreteCategory.hom (R.cohomologyRes F 2)) y) = R.relativeDegree • (σ big) y) {small big : NormalLayer G} (R : LayerRestriction small big) (x : ↑(big.H F' 2)) : (descendedInv φ σ ⋯ hlift hker small) ((CategoryTheory.ConcreteCategory.hom (R.cohomologyRes F' 2)) x) = R.relativeDegree • (descendedInv φ σ ⋯ hlift hker big) x

Restriction multiplies the descended invariant by the relative degree, as it does σ.

@[simp]

theorem TauCeti.ClassFieldTheory.descendedInv_conj {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} (φ : F.toRep ⟶ F'.toRep) (σ : (L : NormalLayer G) → ↑(L.H F 2) →+ AddCircle 1) (hσ : ∀ {old new : NormalLayer G} (T : LayerRefinement old new) (y : ↑(old.H F 2)), (σ new) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F 2)) y) = (σ old) y) (hlift : ∀ (L : NormalLayer G) (x : ↑(L.H F' 2)), ∃ (L' : NormalLayer G) (T : LayerRefinement L L') (y : ↑(L'.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L'.Gal) (L'.repMap φ) 2)) y = (CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F' 2)) x) (hker : ∀ (L : NormalLayer G) (y : ↑(L.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = 0 → (σ L) y = 0) (hconj : ∀ (L : NormalLayer G) (g : G) (y : ↑(L.H F 2)), (σ (L.conjugate g)) ((CategoryTheory.ConcreteCategory.hom (L.conjugateCohomologyIso F g 2).hom) y) = (σ L) y) (L : NormalLayer G) (g : G) (x : ↑(L.H F' 2)) : (descendedInv φ σ ⋯ hlift hker (L.conjugate g)) ((CategoryTheory.ConcreteCategory.hom (L.conjugateCohomologyIso F' g 2).hom) x) = (descendedInv φ σ ⋯ hlift hker L) x

Conjugation preserves the descended invariant, as it does σ.

theorem TauCeti.ClassFieldTheory.descendedInv_injective {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} (φ : F.toRep ⟶ F'.toRep) (σ : (L : NormalLayer G) → ↑(L.H F 2) →+ AddCircle 1) (hσ : ∀ {old new : NormalLayer G} (T : LayerRefinement old new) (y : ↑(old.H F 2)), (σ new) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F 2)) y) = (σ old) y) (hlift : ∀ (L : NormalLayer G) (x : ↑(L.H F' 2)), ∃ (L' : NormalLayer G) (T : LayerRefinement L L') (y : ↑(L'.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L'.Gal) (L'.repMap φ) 2)) y = (CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F' 2)) x) (hker : ∀ (L : NormalLayer G) (y : ↑(L.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = 0 → (σ L) y = 0) (h1 : ∀ (L : NormalLayer G), Subsingleton ↑(L.H F' 1)) (hσ₀ : ∀ (L : NormalLayer G) (y : ↑(L.H F 2)), (σ L) y = 0 → (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = 0) (L : NormalLayer G) : Function.Injective ⇑(descendedInv φ σ ⋯ hlift hker L)

The descended invariant is injective when H¹ of every layer of F' vanishes and σ vanishes only on the classes that φ kills: a class of invariant zero has a lift killed by φ, so its inflation vanishes, and inflation is injective.

theorem TauCeti.ClassFieldTheory.range_descendedInv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} (φ : F.toRep ⟶ F'.toRep) (σ : (L : NormalLayer G) → ↑(L.H F 2) →+ AddCircle 1) (hσ : ∀ {old new : NormalLayer G} (T : LayerRefinement old new) (y : ↑(old.H F 2)), (σ new) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F 2)) y) = (σ old) y) (hlift : ∀ (L : NormalLayer G) (x : ↑(L.H F' 2)), ∃ (L' : NormalLayer G) (T : LayerRefinement L L') (y : ↑(L'.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L'.Gal) (L'.repMap φ) 2)) y = (CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F' 2)) x) (hker : ∀ (L : NormalLayer G) (y : ↑(L.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = 0 → (σ L) y = 0) (h1 : ∀ (L : NormalLayer G), Subsingleton ↑(L.H F' 1)) (hσ₀ : ∀ (L : NormalLayer G) (y : ↑(L.H F 2)), (σ L) y = 0 → (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = 0) (hres : ∀ {small big : NormalLayer G} (R : LayerRestriction small big) (y : ↑(big.H F 2)), (σ small) ((CategoryTheory.ConcreteCategory.hom (R.cohomologyRes F 2)) y) = R.relativeDegree • (σ big) y) (hgen : ∀ (L : NormalLayer G), ∃ (L' : NormalLayer G) (_ : LayerRefinement L L') (y : ↑(L'.H F 2)), (σ L') y = ↑(1 / ↑L.degree)) (L : NormalLayer G) : Set.range ⇑(descendedInv φ σ ⋯ hlift hker L) = ↑(AddSubgroup.torsionBy (AddCircle 1) ↑L.degree)

The image of the descended invariant of a layer of degree n is the n-torsion of ℚ/ℤ when, in addition to the hypotheses of descendedInv_injective, σ multiplies by the relative degree under restriction and every layer, of degree n, has a refinement carrying a class with σ = 1/n.

The class formation of a descended invariant

noncomputable def TauCeti.ClassFieldTheory.ClassFormation.ofDescendedInv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} (φ : F.toRep ⟶ F'.toRep) (σ : (L : NormalLayer G) → ↑(L.H F 2) →+ AddCircle 1) (hσ : ∀ {old new : NormalLayer G} (T : LayerRefinement old new) (y : ↑(old.H F 2)), (σ new) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F 2)) y) = (σ old) y) (hlift : ∀ (L : NormalLayer G) (x : ↑(L.H F' 2)), ∃ (L' : NormalLayer G) (T : LayerRefinement L L') (y : ↑(L'.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L'.Gal) (L'.repMap φ) 2)) y = (CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F' 2)) x) (hker : ∀ (L : NormalLayer G) (y : ↑(L.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = 0 → (σ L) y = 0) (h1 : ∀ (L : NormalLayer G), Subsingleton ↑(L.H F' 1)) (hσ₀ : ∀ (L : NormalLayer G) (y : ↑(L.H F 2)), (σ L) y = 0 → (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = 0) (hres : ∀ {small big : NormalLayer G} (R : LayerRestriction small big) (y : ↑(big.H F 2)), (σ small) ((CategoryTheory.ConcreteCategory.hom (R.cohomologyRes F 2)) y) = R.relativeDegree • (σ big) y) (hconj : ∀ (L : NormalLayer G) (g : G) (y : ↑(L.H F 2)), (σ (L.conjugate g)) ((CategoryTheory.ConcreteCategory.hom (L.conjugateCohomologyIso F g 2).hom) y) = (σ L) y) (hgen : ∀ (L : NormalLayer G), ∃ (L' : NormalLayer G) (_ : LayerRefinement L L') (y : ↑(L'.H F 2)), (σ L') y = ↑(1 / ↑L.degree)) : ClassFormation F'

The class formation of a descended invariant. Let σ be an invariant of the layers of F that does not change under inflation, multiplies by the relative degree under restriction and is preserved by conjugation. Suppose that every class of F' lifts along φ after inflation to a refinement, that σ vanishes exactly on the classes that φ kills, that every layer, of degree n, has a refinement carrying a class with σ = 1/n, and that H¹ of every layer of F' vanishes. Then F' is a class formation, with the descended invariant as its invariant map.

@[simp]

theorem TauCeti.ClassFieldTheory.ClassFormation.ofDescendedInv_inv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} (φ : F.toRep ⟶ F'.toRep) (σ : (L : NormalLayer G) → ↑(L.H F 2) →+ AddCircle 1) (hσ : ∀ {old new : NormalLayer G} (T : LayerRefinement old new) (y : ↑(old.H F 2)), (σ new) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F 2)) y) = (σ old) y) (hlift : ∀ (L : NormalLayer G) (x : ↑(L.H F' 2)), ∃ (L' : NormalLayer G) (T : LayerRefinement L L') (y : ↑(L'.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L'.Gal) (L'.repMap φ) 2)) y = (CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F' 2)) x) (hker : ∀ (L : NormalLayer G) (y : ↑(L.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = 0 → (σ L) y = 0) (h1 : ∀ (L : NormalLayer G), Subsingleton ↑(L.H F' 1)) (hσ₀ : ∀ (L : NormalLayer G) (y : ↑(L.H F 2)), (σ L) y = 0 → (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = 0) (hres : ∀ {small big : NormalLayer G} (R : LayerRestriction small big) (y : ↑(big.H F 2)), (σ small) ((CategoryTheory.ConcreteCategory.hom (R.cohomologyRes F 2)) y) = R.relativeDegree • (σ big) y) (hconj : ∀ (L : NormalLayer G) (g : G) (y : ↑(L.H F 2)), (σ (L.conjugate g)) ((CategoryTheory.ConcreteCategory.hom (L.conjugateCohomologyIso F g 2).hom) y) = (σ L) y) (hgen : ∀ (L : NormalLayer G), ∃ (L' : NormalLayer G) (_ : LayerRefinement L L') (y : ↑(L'.H F 2)), (σ L') y = ↑(1 / ↑L.degree)) : (ofDescendedInv φ σ ⋯ hlift hker h1 hσ₀ ⋯ hconj hgen).inv = descendedInv φ σ ⋯ hlift hker

The invariant map of ClassFormation.ofDescendedInv is the descended invariant.