Formations and their finite normal layers

Artin and Tate describe a formation by a group G, a distinguished family of finite-index subgroups, and a G-module A each of whose elements is fixed by a sufficiently small member of the family. In the arithmetic applications the family is the family of open subgroups of a compact, totally disconnected Galois group and A is a discrete continuous module, so this file uses the topological formulation: a Formation is a smooth discrete topological representation of G over ℤ, and its U-level A^U is the submodule fixed by an open subgroup U.

A finite normal layer is a pair of open subgroups V ≤ U with V normal in U. In field notation it is the layer K/F with U = G_F and V = G_K. Its Galois group Γ = U ⧸ V is finite because V is open in the compact group U, its coefficient module is the level A^V, and its ground level is A^U. The three constructions below are what the cohomology of the layer is taken of and compared with:

• rep, the coefficient module A^V carrying the action of Γ. The U-action on A^V is well defined because V is normal in U, and V acts on A^V trivially, so the action descends to Γ.
• groundLevelEquiv, the identification (A^V)^Γ = A^U of the invariants of the coefficient module with the ground level. Both sides are read inside A^V — the invariants of Γ and the ground level comapped along A^V ⊆ A are the same submodule of A^V — so the identification does not move an element of the ambient module.
• norm, normSubgroup and NormQuotient: the norm N_{U/V} : A^V → A^U, its image, and the quotient A^U / N_{U/V}(A^V).

The additive convention is used throughout, as in the abstract theory; a multiplicative group such as Kˣ enters through an Additive adapter.

Main definitions

• TauCeti.ClassFieldTheory.Formation: a compact, totally disconnected topological group's smooth discrete integral coefficient module.
• TauCeti.ClassFieldTheory.Formation.level: the level A^U of an open subgroup.
• TauCeti.ClassFieldTheory.Formation.levelEquivH0: the level A^U as the degree-zero cohomology H⁰(U, A).
• TauCeti.ClassFieldTheory.NormalLayer: a finite normal layer V ◁ U.
• TauCeti.ClassFieldTheory.NormalLayer.Gal, degree: the Galois group U ⧸ V and its order.
• TauCeti.ClassFieldTheory.NormalLayer.ofOpenNormal: the layer V ◁ ⊤ of an open normal subgroup, with galOfOpenNormalEquiv identifying its Galois group with G ⧸ V.
• TauCeti.ClassFieldTheory.NormalLayer.rep: the coefficient module A^V of the layer, as a representation of U ⧸ V.
• TauCeti.ClassFieldTheory.NormalLayer.coeffFixedPointsEquiv: the coefficient module A^V read as the fixed points M^V when A is read on a G-module M.
• TauCeti.ClassFieldTheory.NormalLayer.H, TateH, TrivialTateH: the ordinary and Tate cohomology carriers of the layer, in the coefficient module A^V and in trivial integral coefficients.
• TauCeti.ClassFieldTheory.NormalLayer.tateHIsoH: the identification of positive-degree Tate cohomology of the layer with its ordinary cohomology.
• TauCeti.ClassFieldTheory.NormalLayer.tateHMinusTwoEquivAbelianization: the identification of degree -2 Tate cohomology with the additive abelianization of the Galois group, normalized so that the Artin map satisfies the character formula.
• TauCeti.ClassFieldTheory.NormalLayer.norm, normSubgroup, NormQuotient, normQuotientMk: the norm of the layer, its image, the norm quotient and the quotient map onto it.
• TauCeti.ClassFieldTheory.NormalLayer.normQuotientEquivOfGroundEquiv: the norm quotient read as A / N through an identification of a group A with the ground level that carries N onto the norm subgroup.
• TauCeti.ClassFieldTheory.NormalLayer.zeroTateClass: the zero-dimensional Tate class of an element of the ground level.

Main statements

• TauCeti.ClassFieldTheory.Formation.exists_mem_level: every element of the coefficient module is fixed by an open subgroup.
• TauCeti.ClassFieldTheory.NormalLayer.groundLevelEquiv: (A^V)^{U/V} ≃ A^U.
• TauCeti.ClassFieldTheory.NormalLayer.tateHMinusTwoEquivAbelianization_single_one: the degree -2 identification sends the standard homology class of g to the class of g⁻¹.
• TauCeti.ClassFieldTheory.NormalLayer.tateHZeroEquivNormQuotient: degree-zero Tate cohomology of the layer is the norm quotient.
• TauCeti.ClassFieldTheory.NormalLayer.zeroTateClass_eq_zero_iff: the zero-dimensional Tate class of an element of the ground level vanishes exactly when the element is a norm.

Implementation notes

The coefficient module is built as Representation.ofQuotient of a Representation.subrepresentation, so that its underlying module is definitionally the level A^V. Mathlib's packaged Rep.quotientToInvariants would instead produce the invariants of the restriction of A along V ∩ U → U → G, which is the same submodule of the ambient module but not the same term as A^V, and every later comparison would have to transport along that equality.

Both Formation and NormalLayer assume that G is compact and totally disconnected. Compactness makes the Galois group of every layer finite, so that the degree of a layer is its genuine index and not the junk value 0 of an infinite quotient.

Both the group and the coefficient module live in Type. Mathlib's tateCohomology asks for the finite group and the coefficient ring ℤ in one universe and for the coefficient module in that same universe, and every carrier of the arithmetic instances is a Type, so nothing is lost.

The coefficient module is read as a plain Rep ℤ G through Representation.ofDistribMulAction at the action TopRep.distribMulAction derives from the operators of the topological representation. Passing instead through ContRepresentation.toRepresentation would carry the Module ℤ instance packaged inside TopRep, which is not the instance AddCommGroup.toIntModule that typeclass synthesis produces for an integral module, and the two are not definitionally equal.

Because toRep and rep are abbrevs for Rep.of, simp reduces the carriers F.toRep.V and (L.rep F).V to F.module.V and F.level L.top wherever they occur as implicit type arguments (the type of a coercion, of a bundled map, of a membership) before it looks a term up among its lemmas. A simp lemma is indexed by its left-hand side as elaborated, where these carriers are still unreduced, so a lemma stated plainly over F.toRep.V is never found. The simp lemmas about levels, layer coefficients and the norm below therefore state their left-hand sides through dsimp% only, which puts those implicit arguments in the form simp produces. Only the left-hand side is wrapped, and with only, so that the right-hand side keeps the form it is written in: rw with these lemmas then leaves terms over F.toRep, as the rest of this file states them.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV.
• J. Neukirch, Class Field Theory, Chapter III.
• J.-P. Serre, Local Fields, Chapter XI.

Formations and their levels

@[reducible, inline]

abbrev TauCeti.ClassFieldTheory.Formation (G : Type) [Group G] [TopologicalSpace G] [_tg : IsTopologicalGroup G] [_cs : CompactSpace G] [_td : TotallyDisconnectedSpace G] : Type 1

A formation: a smooth discrete continuous integral representation of a compact, totally disconnected topological group. In the arithmetic applications G is the Galois group of a Galois extension and the module is the multiplicative group of the top field, read additively. The distinguished family of subgroups of the Artin–Tate definition is the family of open subgroups of G, which is why the levels below are indexed by OpenSubgroup G. A formation is definitionally the same type as SmoothDiscreteTopRep ℤ G, specialized to integral coefficients and to a profinite group; it introduces no second representation bundle.

@[reducible, inline]

abbrev TauCeti.ClassFieldTheory.Formation.module {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) : TopRep ℤ G

The coefficient module of a formation, as a topological representation of G over ℤ.

@[reducible, inline]

abbrev TauCeti.ClassFieldTheory.Formation.smooth {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) : IsSmoothDiscrete ℤ F.module

The coefficient module is discrete with open point stabilizers.

theorem TauCeti.ClassFieldTheory.Formation.ext {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} (h : F.module = F'.module) : F = F'

Two formations on G with the same coefficient module are equal.

theorem TauCeti.ClassFieldTheory.Formation.ext_iff {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} : F = F' ↔ F.module = F'.module

@[reducible, inline]

abbrev TauCeti.ClassFieldTheory.Formation.toRep {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) : Rep ℤ G

The coefficient module of a formation as a plain integral representation of G, forgetting its topology. The levels, the layer representations and all of their cohomology are taken of this underlying representation. Being an abbrev, its carrier is reduced by simp; see the implementation notes for how simp lemmas over it are stated.

theorem TauCeti.ClassFieldTheory.Formation.toRep_ρ_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (g : G) (x : ↑F.toRep) : (F.toRep.ρ g) x = (F.module.ρ g) x

An element g acts on the underlying representation F.toRep as it acts on the coefficient module.

noncomputable def TauCeti.ClassFieldTheory.Formation.level {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (U : OpenSubgroup G) : Submodule ℤ ↑F.toRep

The level A^U of an open subgroup U, as a submodule of the ambient module of the formation. Keeping every level inside one ambient module is what makes the inclusion of a level in a smaller subgroup's level, and the norm between two levels, maps of submodules of a fixed module.

@[simp]

theorem TauCeti.ClassFieldTheory.Formation.mem_level {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) {U : OpenSubgroup G} {x : ↑F.toRep} : x ∈ F.level U ↔ ∀ u ∈ U, (F.toRep.ρ u) x = x

An element lies in the level A^U exactly when every element of U fixes it.

theorem TauCeti.ClassFieldTheory.Formation.exists_mem_level {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (x : ↑F.toRep) : ∃ (U : OpenSubgroup G), x ∈ F.level U

Every element of the coefficient module lies in a level. This is the Artin–Tate condition that each element of A is fixed by a sufficiently small member of the distinguished family of subgroups, and it is exactly what smoothness of the module supplies: the stabilizer of an element is open.

theorem TauCeti.ClassFieldTheory.Formation.level_antitone {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) : Antitone F.level

Levels decrease as the subgroup grows: a larger subgroup fixes fewer elements.

noncomputable def TauCeti.ClassFieldTheory.Formation.levelEquivH0 {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (U : OpenSubgroup G) : ↥(F.level U) ≃+ ↥(ContCohomology.H0 ↥↑U ↑F.toRep)

The level A^U of an open subgroup is the degree-zero cohomology H⁰(U, A) of U acting on the coefficient module: both are the elements of the ambient module fixed by U, and the equivalence moves none of them.

@[simp]

theorem TauCeti.ClassFieldTheory.Formation.levelEquivH0_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (U : OpenSubgroup G) (x : ↥(F.level U)) : ↑((F.levelEquivH0 U) x) = ↑x

levelEquivH0 moves no element of the ambient module.

@[simp]

theorem TauCeti.ClassFieldTheory.Formation.levelEquivH0_symm_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (U : OpenSubgroup G) (x : ↥(ContCohomology.H0 ↥↑U ↑F.toRep)) : ↑((F.levelEquivH0 U).symm x) = ↑x

The inverse of levelEquivH0 moves no element of the ambient module either.

Finite normal layers

structure TauCeti.ClassFieldTheory.NormalLayer (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : Type

A finite normal layer V ◁ U of open subgroups of G. In field notation this is the finite Galois layer K/F inside the extension G cuts out, with U = G_F the ground subgroup and V = G_K the top subgroup.

• ground : OpenSubgroup G

  the ground subgroup U, cutting out the base field of the layer

• top : OpenSubgroup G

  the top subgroup V, cutting out the top field of the layer

• top_le_ground : self.top ≤ self.ground

  the layer runs upwards: V ≤ U

• normal : ((↑self.top).subgroupOf ↑self.ground).Normal

  V is normal in U, so that the layer is Galois

theorem TauCeti.ClassFieldTheory.NormalLayer.ext_iff {G : Type} {inst✝ : Group G} {inst✝¹ : TopologicalSpace G} {inst✝² : IsTopologicalGroup G} {inst✝³ : CompactSpace G} {inst✝⁴ : TotallyDisconnectedSpace G} {x y : NormalLayer G} : x = y ↔ x.ground = y.ground ∧ x.top = y.top

theorem TauCeti.ClassFieldTheory.NormalLayer.ext {G : Type} {inst✝ : Group G} {inst✝¹ : TopologicalSpace G} {inst✝² : IsTopologicalGroup G} {inst✝³ : CompactSpace G} {inst✝⁴ : TotallyDisconnectedSpace G} {x y : NormalLayer G} (ground : x.ground = y.ground) (top : x.top = y.top) : x = y

@[reducible, inline]

abbrev TauCeti.ClassFieldTheory.NormalLayer.relativeTop {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) : Subgroup ↥L.ground

The top subgroup V of a layer, viewed as a subgroup of the ground subgroup U.

instance TauCeti.ClassFieldTheory.NormalLayer.instNormalSubtypeMemOpenSubgroupGroundRelativeTop {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) : L.relativeTop.Normal

The top subgroup of a layer is normal in the ground subgroup.

@[reducible, inline]

abbrev TauCeti.ClassFieldTheory.NormalLayer.Gal {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) : Type

The Galois group Γ = U ⧸ V of a finite normal layer.

theorem TauCeti.ClassFieldTheory.NormalLayer.conj_mem_top {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) {u : G} (hu : u ∈ L.ground) {v : G} (hv : v ∈ L.top) : u * v * u⁻¹ ∈ L.top

The top subgroup of a layer is normal in the ground subgroup, read on elements of G.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.degree {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) : ℕ

The degree [U : V] of a normal layer, the index of the top subgroup in the ground subgroup.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.degree_eq_natCard_gal {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) : L.degree = Nat.card L.Gal

The degree of a layer is the order of its Galois group U ⧸ V.

theorem TauCeti.ClassFieldTheory.NormalLayer.degree_eq_relIndex {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) : L.degree = (↑L.top).relIndex ↑L.ground

The degree of a layer is the relative index of its top subgroup in its ground subgroup.

def TauCeti.ClassFieldTheory.NormalLayer.ofOpenNormal {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (V : OpenNormalSubgroup G) : NormalLayer G

The layer V ◁ ⊤ cut out by an open normal subgroup of G. These layers are the finite Galois extensions of the ground field of a formation on G.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.ground_ofOpenNormal {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (V : OpenNormalSubgroup G) : (ofOpenNormal V).ground = ⊤

The ground subgroup of the layer V ◁ ⊤ is all of G.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.top_ofOpenNormal {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (V : OpenNormalSubgroup G) : (ofOpenNormal V).top = V.toOpenSubgroup

The top subgroup of the layer V ◁ ⊤ is V.

def TauCeti.ClassFieldTheory.NormalLayer.galOfOpenNormalEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (V : OpenNormalSubgroup G) : (ofOpenNormal V).Gal ≃* G ⧸ ↑V.toOpenSubgroup

The Galois group of the layer V ◁ ⊤ is the finite quotient G ⧸ V.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.galOfOpenNormalEquiv_mk {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (V : OpenNormalSubgroup G) (u : ↥(ofOpenNormal V).ground) : (galOfOpenNormalEquiv V) ↑u = ↑↑u

The identification of the Galois group of V ◁ ⊤ with G ⧸ V sends the class of u to the class of u.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.galOfOpenNormalEquiv_symm_mk {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (V : OpenNormalSubgroup G) (u : ↥(ofOpenNormal V).ground) : (galOfOpenNormalEquiv V).symm ↑↑u = ↑u

The inverse identification of G ⧸ V with the Galois group of V ◁ ⊤ sends the class of u to the class of u.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.groundEquivOfOpenNormal {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (V : OpenNormalSubgroup G) : ↥(F.level ⊤) ≃ₗ[ℤ] ↥(F.level (ofOpenNormal V).ground)

The ground level of the layer V ◁ G of an open normal subgroup V is the level A^G of the whole group.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.groundEquivOfOpenNormal_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (V : OpenNormalSubgroup G) (a : ↥(F.level ⊤)) : ↑((groundEquivOfOpenNormal F V) a) = ↑a

The identification of A^G with the ground level of V ◁ G moves no element of the ambient module.

instance TauCeti.ClassFieldTheory.NormalLayer.instFiniteGal {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) : Finite L.Gal

The top subgroup is open in the compact ground subgroup, so the Galois group is finite.

@[instance_reducible]

noncomputable instance TauCeti.ClassFieldTheory.NormalLayer.instFintypeGal {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) : Fintype L.Gal

The Galois group of a layer is finite, so it carries a Fintype structure.

instance TauCeti.ClassFieldTheory.NormalLayer.instNormalSubgroupOf {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) : ((↑L.top).subgroupOf ↑L.ground).Normal

The top subgroup of a layer is normal in the ground subgroup, stated for the underlying subgroups of G: this is the form in which the continuous cohomology of the ground subgroup L.ground.toSubgroup takes it.

instance TauCeti.ClassFieldTheory.NormalLayer.instDiscreteTopologyQuotient {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) : DiscreteTopology (↥↑L.ground ⧸ (↑L.top).subgroupOf ↑L.ground)

The top subgroup is open in the ground subgroup, so the Galois group, presented as the quotient of the underlying subgroup L.ground.toSubgroup of G, is discrete.

theorem TauCeti.ClassFieldTheory.NormalLayer.degree_pos {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) : 0 < L.degree

The degree of a layer is positive.

The coefficient module of a layer

theorem TauCeti.ClassFieldTheory.NormalLayer.level_top_le_comap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (u : ↥L.ground) : F.level L.top ≤ Submodule.comap (F.toRep.ρ ↑u) (F.level L.top)

The ground subgroup carries the top level into itself: this is exactly normality of V in U.

@[reducible, inline]

noncomputable abbrev TauCeti.ClassFieldTheory.NormalLayer.groundRep {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) : Representation ℤ ↥L.ground ↥(F.level L.top)

The action of the ground subgroup U on the top level A^V.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.groundRep_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (u : ↥L.ground) (x : ↥(F.level L.top)) : ↑(((L.groundRep F) u) x) = (F.toRep.ρ ↑u) ↑x

The ground subgroup acts on the top level by the restriction of the action on the ambient module.

instance TauCeti.ClassFieldTheory.NormalLayer.instIsTrivialIntSubtypeMemOpenSubgroupGroundSubgroupRelativeTopVToRepSubmoduleLevelTopCompLinearMapIdGroundRepSubtype {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) : Representation.IsTrivial (MonoidHom.comp (L.groundRep F) L.relativeTop.subtype)

The top subgroup acts trivially on the top level, so the U-action descends to U ⧸ V.

@[reducible, inline]

noncomputable abbrev TauCeti.ClassFieldTheory.NormalLayer.rep {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) : Rep ℤ L.Gal

The coefficient module of a layer: the top level A^V with the induced action of the Galois group U ⧸ V. Its underlying module is the level itself, not an isomorphic copy.

theorem TauCeti.ClassFieldTheory.NormalLayer.rep_ρ_mk_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (u : ↥L.ground) (x : ↥(F.level L.top)) : ↑(((L.rep F).ρ ↑u) x) = (F.toRep.ρ ↑u) ↑x

The class of u ∈ U in the Galois group acts on the coefficient module of the layer as u acts on the ambient module.

theorem TauCeti.ClassFieldTheory.NormalLayer.level_ground_le_level_top {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) : F.level L.ground ≤ F.level L.top

The ground level sits inside the top level.

theorem TauCeti.ClassFieldTheory.NormalLayer.invariants_rep {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) : (L.rep F).ρ.invariants = Submodule.comap (F.level L.top).subtype (F.level L.ground)

The invariants of the coefficient module are the ground level: (A^V)^{U/V} = A^U. Both sides are read inside the top level A^V.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.groundLevelEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) : ↥(L.rep F).ρ.invariants ≃ₗ[ℤ] ↥(F.level L.ground)

The identification (A^V)^{U/V} ≃ A^U of the invariants of the coefficient module with the ground level. It moves no element of the ambient module.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.groundLevelEquiv_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (x : ↥(L.rep F).ρ.invariants) : ↑((L.groundLevelEquiv F) x) = ↑↑x

groundLevelEquiv moves no element of the ambient module.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.groundLevelEquiv_symm_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (y : ↥(F.level L.ground)) : ↑↑((L.groundLevelEquiv F).symm y) = ↑y

The inverse of groundLevelEquiv moves no element of the ambient module either.

def TauCeti.ClassFieldTheory.NormalLayer.coeffFixedPointsEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) {F : Formation G} {M : Type} [AddCommGroup M] [DistribMulAction G M] (e : M ≃+ ↑F.toRep) (he : ∀ (g : G) (x : M), e (g • x) = (F.toRep.ρ g) (e x)) : ↑(L.rep F) ≃+ ↥(FixedPoints.addSubgroup (↥((↑L.top).subgroupOf ↑L.ground)) M)

The coefficient module of a layer read in a G-module: when the coefficient module of the formation is read, through an equivariant additive equivalence e : M ≃+ A, on a G-module M, the coefficient module A^V of a layer V ◁ U is the subgroup M^V of fixed points of its top subgroup, viewed as a subgroup of the ground subgroup U. It only changes the coefficient dictionary (coeffFixedPointsEquiv_apply_coe) and is equivariant for the Galois group of the layer (coeffFixedPointsEquiv_ρ).

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.coeffFixedPointsEquiv_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) {F : Formation G} {M : Type} [AddCommGroup M] [DistribMulAction G M] (e : M ≃+ ↑F.toRep) (he : ∀ (g : G) (x : M), e (g • x) = (F.toRep.ρ g) (e x)) (x : ↑(L.rep F)) : ↑((L.coeffFixedPointsEquiv e he) x) = e.symm ↑x

coeffFixedPointsEquiv reads an element of the coefficient module in M through e.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.coeffFixedPointsEquiv_symm_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) {F : Formation G} {M : Type} [AddCommGroup M] [DistribMulAction G M] (e : M ≃+ ↑F.toRep) (he : ∀ (g : G) (x : M), e (g • x) = (F.toRep.ρ g) (e x)) (m : ↥(FixedPoints.addSubgroup (↥((↑L.top).subgroupOf ↑L.ground)) M)) : ↑((L.coeffFixedPointsEquiv e he).symm m) = e ↑m

The inverse of coeffFixedPointsEquiv reads a fixed point of M in the coefficient module through e.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.coeffFixedPointsEquiv_ρ {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) {F : Formation G} {M : Type} [AddCommGroup M] [DistribMulAction G M] (e : M ≃+ ↑F.toRep) (he : ∀ (g : G) (x : M), e (g • x) = (F.toRep.ρ g) (e x)) (g : ↥↑L.ground ⧸ (↑L.top).subgroupOf ↑L.ground) (x : ↑(L.rep F)) : (L.coeffFixedPointsEquiv e he) (((L.rep F).ρ g) x) = g • (L.coeffFixedPointsEquiv e he) x

coeffFixedPointsEquiv is equivariant for the Galois group of the layer.

The cohomology of a layer

@[reducible, inline]

noncomputable abbrev TauCeti.ClassFieldTheory.NormalLayer.H {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (n : ℕ) : ModuleCat ℤ

Ordinary group cohomology of a finite normal layer, H^n(U/V, A^V), on Mathlib's carrier. The axioms satisfied by a class formation and the fundamental class of a layer are read here.

@[reducible, inline]

noncomputable abbrev TauCeti.ClassFieldTheory.NormalLayer.TateH {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (r : ℤ) : ModuleCat ℤ

Tate cohomology of a finite normal layer in its coefficient module, the Tate group H^r(U/V, A^V) in every integer degree r.

@[reducible, inline]

noncomputable abbrev TauCeti.ClassFieldTheory.NormalLayer.TrivialTateH {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (r : ℤ) : ModuleCat ℤ

Tate cohomology of a finite normal layer with trivial integral coefficients, the Tate group H^r(U/V, ℤ). Its degree -2 is the abelianization of the Galois group of the layer. In a class formation, cup product with the fundamental class of the layer carries that degree isomorphically onto TateH in degree 0, and the Artin map is the inverse of this isomorphism.

@[reducible, inline]

noncomputable abbrev TauCeti.ClassFieldTheory.NormalLayer.TrivialH {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (n : ℕ) : ModuleCat ℤ

Ordinary cohomology of a finite normal layer with trivial integral coefficients, H^n(U/V, ℤ). This is the positive-degree comparison target for TrivialTateH.

The two low Tate degrees

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.tateHMinusTwoEquivAbelianization {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) : ↑(L.TrivialTateH (-2)) ≃+ Additive (Abelianization L.Gal)

Degree -2 Tate cohomology with trivial integral coefficients is the additive abelianization of the Galois group. This is the source of the Galois side of the Nakayama map.

It is the negative of the generic identification TauCeti.TateCohomology.HNegTwoAddEquivAbelianization, so the first-homology class of (g, 1) goes to g⁻¹ (tateHMinusTwoEquivAbelianization_single_one). With the generic identification the Tate pairing of σ ∈ Γ^ab with the connecting class δχ of a character is -χ(σ) (TauCeti.TateCohomology.toRatAddCircle_map_leftUnitor_cup_characterConnectingClass). With this sign it is χ(σ), and the Artin map satisfies the classical character formula χ(artinMap a) = inv(a₀ ∪ δχ) instead of being the inverse of the classical reciprocity map.

theorem TauCeti.ClassFieldTheory.NormalLayer.tateHMinusTwoEquivAbelianization_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (x : ↑(L.TrivialTateH (-2))) : L.tateHMinusTwoEquivAbelianization x = -TateCohomology.HNegTwoAddEquivAbelianization x

The layer's degree--2 identification is the negative of the generic identification for its Galois group.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.tateHMinusTwoEquivAbelianization_single_one {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : L.Gal) : L.tateHMinusTwoEquivAbelianization ((CategoryTheory.ConcreteCategory.hom ((TateCohomology.isoGroupHomology (-2) 1 ⋯).inv.app (Rep.trivial ℤ L.Gal ℤ))) ((CategoryTheory.ConcreteCategory.hom (groupHomology.H1π (Rep.trivial ℤ L.Gal ℤ))) ((CategoryTheory.ConcreteCategory.hom (groupHomology.cycles₁IsoOfIsTrivial (Rep.trivial ℤ L.Gal ℤ)).inv) (Finsupp.single g 1)))) = Additive.ofMul (Abelianization.of g⁻¹)

The degree -2 identification sends the standard first-homology class represented by (g, 1) to the class of g⁻¹ in the additive abelianization.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.tateHMinusTwoEquivAbelianization_symm_of {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : L.Gal) : L.tateHMinusTwoEquivAbelianization.symm (Additive.ofMul (Abelianization.of g)) = (CategoryTheory.ConcreteCategory.hom ((TateCohomology.isoGroupHomology (-2) 1 ⋯).inv.app (Rep.trivial ℤ L.Gal ℤ))) ((CategoryTheory.ConcreteCategory.hom (groupHomology.H1π (Rep.trivial ℤ L.Gal ℤ))) ((CategoryTheory.ConcreteCategory.hom (groupHomology.cycles₁IsoOfIsTrivial (Rep.trivial ℤ L.Gal ℤ)).inv) (Finsupp.single g⁻¹ 1)))

The inverse degree -2 identification sends the abelianization class of g to the standard first-homology class represented by (g⁻¹, 1).

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.tateHIsoH {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (r : ℕ) [NeZero r] : L.TateH F ↑r ≅ L.H F r

In positive degrees the Tate cohomology of a finite normal layer is its ordinary cohomology. This is Mathlib's comparison TateCohomology.isoGroupCohomology, stated between the carriers TateH and H of the layer, so that it composes with maps between those carriers.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.trivialTateHIsoH {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (r : ℕ) [NeZero r] : L.TrivialTateH ↑r ≅ L.TrivialH r

In positive degrees Tate cohomology with trivial integral coefficients is ordinary cohomology.

theorem TauCeti.ClassFieldTheory.NormalLayer.trivialTateHIsoH_def {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (r : ℕ) [NeZero r] : L.trivialTateHIsoH r = (TateCohomology.isoGroupCohomology r).app (Rep.trivial ℤ L.Gal ℤ)

The positive-degree comparison for trivial coefficients is Mathlib's canonical comparison isomorphism.

theorem TauCeti.ClassFieldTheory.NormalLayer.tateHIsoH_def {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (r : ℕ) [NeZero r] : L.tateHIsoH F r = (TateCohomology.isoGroupCohomology r).app (L.rep F)

The identification of positive-degree Tate cohomology of a layer with its ordinary cohomology is Mathlib's comparison isomorphism at the coefficient module of the layer.

The norm of a layer

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.norm {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) : ↥(F.level L.top) →ₗ[ℤ] ↥(F.level L.ground)

The norm N_{U/V} : A^V → A^U of a finite normal layer: the sum of the Galois conjugates, landing in the ground level through groundLevelEquiv.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.norm_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (x : ↥(F.level L.top)) : ↑((L.norm F) x) = ∑ γ : L.Gal, ↑(((L.rep F).ρ γ) x)

The norm of a layer is the sum of the Galois conjugates: N_{U/V}(x) = ∑_{γ ∈ U ⧸ V} γ x.

theorem TauCeti.ClassFieldTheory.NormalLayer.norm_apply_coe_of_mem_level_ground {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (x : ↥(F.level L.top)) (hx : ↑x ∈ F.level L.ground) : ↑((L.norm F) x) = L.degree • ↑x

The norm of a layer is the trace of the Galois action on the top level, so on an element of the ground level it is multiplication by the degree.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.normSubgroup {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) : Submodule ℤ ↥(F.level L.ground)

The norm subgroup N_{U/V}(A^V) of the ground level.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.mem_normSubgroup {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) {y : ↥(F.level L.ground)} : y ∈ L.normSubgroup F ↔ ∃ (x : ↥(F.level L.top)), (L.norm F) x = y

An element of the ground level lies in the norm subgroup exactly when it is a norm.

@[reducible, inline]

abbrev TauCeti.ClassFieldTheory.NormalLayer.NormQuotient {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) : Type

The norm quotient A^U / N_{U/V}(A^V) of a finite normal layer. It is the group that the Artin map of a class formation — a formation whose layers satisfy the axioms on H¹ and H², which a bare Formation does not assume — identifies with the abelianization of the Galois group of the layer.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.normQuotientMk {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) : ↥(F.level L.ground) →ₗ[ℤ] L.NormQuotient F

The canonical map from the ground level onto the norm quotient. The Artin map of a class formation is defined on the ground level by composing with this map.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.normQuotientMk_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (x : ↥(F.level L.ground)) : (L.normQuotientMk F) x = Submodule.Quotient.mk x

normQuotientMk sends an element of the ground level to its class in the norm quotient.

theorem TauCeti.ClassFieldTheory.NormalLayer.map_groundLevelEquiv_submoduleOf {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) : Submodule.map (↑(L.groundLevelEquiv F)) ((LinearMap.range (L.rep F).ρ.norm).submoduleOf (L.rep F).ρ.invariants) = L.normSubgroup F

The image under groundLevelEquiv of the norm image inside the invariants is the norm subgroup.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.tateHZeroEquivNormQuotient {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) : ↑(L.TateH F 0) ≃+ L.NormQuotient F

Degree-zero Tate cohomology of a finite normal layer is its norm quotient. This is the low-degree identification that the Artin map of a class formation is read through.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.tateHZeroEquivNormQuotient_H0π {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (x : ↥(L.rep F).ρ.invariants) : (L.tateHZeroEquivNormQuotient F) ((CategoryTheory.ConcreteCategory.hom (TateCohomology.H0π (L.rep F))) x) = (L.normQuotientMk F) ((L.groundLevelEquiv F) x)

The identification of degree-zero Tate cohomology with the norm quotient sends the class of an invariant to the class of the corresponding element of the ground level.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.zeroTateClass {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) : ↥(F.level L.ground) →+ ↑(L.TateH F 0)

The zero-dimensional Tate class a₀ of an element a of the ground level A^U: the class of a in the degree-zero Tate group H^0(U/V, A^V), reading a as an invariant of the coefficient module A^V.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.zeroTateClass_groundLevelEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (x : ↥(L.rep F).ρ.invariants) : (L.zeroTateClass F) ((L.groundLevelEquiv F) x) = (CategoryTheory.ConcreteCategory.hom (TateCohomology.H0π (L.rep F))) x

The zero-dimensional Tate class of the ground-level element corresponding to an invariant is the class of that invariant.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.tateHZeroEquivNormQuotient_zeroTateClass {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (a : ↥(F.level L.ground)) : (L.tateHZeroEquivNormQuotient F) ((L.zeroTateClass F) a) = (L.normQuotientMk F) a

Under the identification of degree-zero Tate cohomology with the norm quotient, the zero-dimensional Tate class of a is the class of a modulo norms.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.zeroTateClass_eq_zero_iff {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (a : ↥(F.level L.ground)) : (L.zeroTateClass F) a = 0 ↔ a ∈ L.normSubgroup F

The zero-dimensional Tate class of a vanishes exactly when a is a norm.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.normQuotientEquivOfGroundEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) {A : Type u_1} [Group A] {N : Subgroup A} (e : Additive A ≃+ ↥(F.level L.ground)) [N.Normal] (hN : ∀ (a : A), e (Additive.ofMul a) ∈ L.normSubgroup F ↔ a ∈ N) : Additive (A ⧸ N) ≃+ L.NormQuotient F

The norm quotient read through an identification of the ground level: if e identifies a group A with the ground level A^U of the layer and carries the normal subgroup N onto the norm subgroup N_{U/V}(A^V), then e descends to an identification of A / N with the norm quotient.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.normQuotientEquivOfGroundEquiv_mk {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) {A : Type u_1} [Group A] {N : Subgroup A} (e : Additive A ≃+ ↥(F.level L.ground)) [N.Normal] (hN : ∀ (a : A), e (Additive.ofMul a) ∈ L.normSubgroup F ↔ a ∈ N) (a : A) : (L.normQuotientEquivOfGroundEquiv F e hN) (Additive.ofMul ↑a) = (L.normQuotientMk F) (e (Additive.ofMul a))

normQuotientEquivOfGroundEquiv sends the class of a ∈ A to the class of e a in the norm quotient.