The profinite tame group Ttame and its unramified marking (Stage C, work order C2)

This file realises the manuscript's finite-quotient tame group T_A = ⟨σ, τ ∣ τ^σ = τ²⟩_prof (reference/q2_manuscript.tex, l.401, Lemma 3.1 lem:tamefinite, Prop 3.2 prop:tamequotient, Lemma 3.3 lem:o2tame) as the cofiltered inverse limit, in ProfiniteGrp, of all finite marked tame quotients — exactly mirroring the Stage-B construction of Γ_A in Candidate/AdmissibleCat.lean + Candidate/GammaA.lean, but with the 2-generator tame marking (s, t) in place of the 4-generator admissible marking q : Gen → Fin n.

Main contents:

• TameMarkedFinite — a concrete tame-marked finite group on the skeleton Fin n (generators s, t, generating, with rconj t s = t²).
• TameHom + Category TameMarkedFinite — generator-preserving homs and the index category; tameHom_ext (any two parallel arrows are equal, the marking generates), binary subdirect objects (tameSubdirectObj), and IsCofiltered TameMarkedFinite.
• tameDiagram : TameMarkedFinite ⥤ ProfiniteGrp, Ttame := Limits.limit tameDiagram, the universal generators tameSigma, tameTau : Ttame, their projection-eval lemmas, the coordinatewise tame relation Ttame_tameRel, and dense generation tameGen_topologically_generate.
• nu_t : Ttame ⟶ ProfiniteZ2 — the unramified character σ ↦ 1, τ ↦ 0 (τ is pro-odd, killed in the unramified pro-2 quotient). Built as the map into the limit ℤ₂ induced by the per-layer projections through the auxiliary cyclic 2-group tame quotients cyclicTame n (carrier C2Pow n, s = additive generator, t = 1). This realises Lemma 3.1's "every normal 2-subgroup is central + unramified" structurally: the only pro-2 information in a tame quotient is the unramified σ-direction.

Instance gotcha (inherited from AdmissibleIndex.lean)

Fin n carries the global Fin.instMul, not the transported group structure A.groupFin. We thread A.groupFin explicitly (@, projection access) through every Fin-level construction so Fin.instMul is never synthesized.

The tame-marked finite index objects

structure Q2Presentation.TameMarkedFinite : Type

A concrete tame-marked finite group with carrier the skeleton Fin n: size n, nonemptiness 0 < n, group structure groupFin, two marked generators s, t, a proof they generate, and the tame relation τ^σ = τ² (rconj t s = t²).

• n : ℕ

  Cardinality of the skeletal carrier.

• hn : Fact (0 < self.n)

  The carrier is nonempty.

• groupFin : Group (Fin self.n)

  The group structure on the skeletal carrier Fin n.

• s : Fin self.n

  The marked tame inertia-free generator σ.

• t : Fin self.n

  The marked tame inertia generator τ.

• generates : Subgroup.closure {self.s, self.t} = ⊤

  s, t generate the carrier.

• tame : rconj self.t self.s = self.t ^ 2

  The tame relation τ^σ = τ².

Generic transport lemmas (no Fin.instMul)

theorem Q2Presentation.rconj_map {G : Type u_1} {H : Type u_2} [Group G] [Group H] {F : Type u_3} [FunLike F G H] [MonoidHomClass F G H] (f : F) (x g : G) : f (rconj x g) = rconj (f x) (f g)

Right conjugation commutes with any monoid homomorphism.

theorem Q2Presentation.tame_generates_transport {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) {s t : G} (hgen : Subgroup.closure {s, t} = ⊤) : Subgroup.closure {e s, e t} = ⊤

Generation transports along a multiplicative equivalence.

theorem Q2Presentation.tame_relation_transport {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) {s t : G} (htame : rconj t s = t ^ 2) : rconj (e t) (e s) = e t ^ 2

The tame relation transports along a multiplicative equivalence.

Skeletalization of an arbitrary tame-marked finite group

noncomputable def Q2Presentation.tameSkeletalize (G : Type u_1) [Group G] [Finite G] [Nonempty G] (s t : G) (hgen : Subgroup.closure {s, t} = ⊤) (htame : rconj t s = t ^ 2) : TameMarkedFinite

Skeletalization. Any tame marking (s, t) of an arbitrary nonempty finite group G is realised by a TameMarkedFinite on Fin (Nat.card G), transporting G's group structure along Finite.equivFin G (mirrors AdmissibleIndex.skeletalize).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Q2Presentation.tameSkelEquiv (G : Type u_1) [Group G] [Finite G] [Nonempty G] (s t : G) (hgen : Subgroup.closure {s, t} = ⊤) (htame : rconj t s = t ^ 2) : Fin (tameSkeletalize G s t hgen htame).n ≃* G

The transport equivalence underlying tameSkeletalize, as a MulEquiv Fin (tameSkeletalize G s t hgen htame).n ≃* G (mirrors skelEquiv).

Equations

• Q2Presentation.tameSkelEquiv G s t hgen htame = (Finite.equivFin G).symm.mulEquiv

@[simp]

theorem Q2Presentation.tameSkelEquiv_s {G : Type u_1} [Group G] [Finite G] [Nonempty G] {s t : G} {hgen : Subgroup.closure {s, t} = ⊤} {htame : rconj t s = t ^ 2} : (tameSkelEquiv G s t hgen htame) (tameSkeletalize G s t hgen htame).s = s

@[simp]

theorem Q2Presentation.tameSkelEquiv_t {G : Type u_1} [Group G] [Finite G] [Nonempty G] {s t : G} {hgen : Subgroup.closure {s, t} = ⊤} {htame : rconj t s = t ^ 2} : (tameSkelEquiv G s t hgen htame) (tameSkeletalize G s t hgen htame).t = t

The generator-preserving morphism category

structure Q2Presentation.TameHom (A B : TameMarkedFinite) : Type

A generator-preserving morphism of tame indices: a homomorphism of the skeletal carriers intertwining the two markings s, t.

• toMonoidHom : Fin A.n →* Fin B.n

  The underlying homomorphism of skeletal carriers.

• map_s : self.toMonoidHom A.s = B.s

  σ-preservation.

• map_t : self.toMonoidHom A.t = B.t

  τ-preservation.

theorem Q2Presentation.TameHom.ext' {A B : TameMarkedFinite} {f g : TameHom A B} (h : f.toMonoidHom = g.toMonoidHom) : f = g

theorem Q2Presentation.TameHom.ext'_iff {A B : TameMarkedFinite} {f g : TameHom A B} : f = g ↔ f.toMonoidHom = g.toMonoidHom

def Q2Presentation.TameHom.id (A : TameMarkedFinite) : TameHom A A

The identity tame hom.

Equations

• Q2Presentation.TameHom.id A = { toMonoidHom := MonoidHom.id (Fin A.n), map_s := ⋯, map_t := ⋯ }

def Q2Presentation.TameHom.comp {A B C : TameMarkedFinite} (f : TameHom A B) (g : TameHom B C) : TameHom A C

Composition of tame homs.

Equations

• f.comp g = { toMonoidHom := g.toMonoidHom.comp f.toMonoidHom, map_s := ⋯, map_t := ⋯ }

instance Q2Presentation.instCategoryTameMarkedFinite : CategoryTheory.Category.{0, 0} TameMarkedFinite

The tame index category.

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.tameHom_ext {A B : TameMarkedFinite} (f g : A ⟶ B) : f = g

Uniqueness of tame morphisms. Both arrows send s, t to B.s, B.t, and s, t generate A, so they agree on a generating set, hence everywhere.

noncomputable def Q2Presentation.tameSkeletalizeHomOut {G : Type u_1} [Group G] [Finite G] [Nonempty G] {s t : G} {hgen : Subgroup.closure {s, t} = ⊤} {htame : rconj t s = t ^ 2} {D : TameMarkedFinite} (ψ : G →* Fin D.n) (hψs : ψ s = D.s) (hψt : ψ t = D.t) : TameHom (tameSkeletalize G s t hgen htame) D

A marking-preserving hom ψ : G →* Fin D.n out of G induces a tame morphism tameSkeletalize G s t hgen htame ⟶ D (mirrors skeletalizeHomOut).

Equations

• Q2Presentation.tameSkeletalizeHomOut ψ hψs hψt = { toMonoidHom := ψ.comp (Q2Presentation.tameSkelEquiv G s t hgen htame).toMonoidHom, map_s := ⋯, map_t := ⋯ }

noncomputable def Q2Presentation.tameSkelHomBetween {G : Type u_1} {H : Type u_2} [Group G] [Finite G] [Nonempty G] [Group H] [Finite H] [Nonempty H] {sG tG : G} {hgG : Subgroup.closure {sG, tG} = ⊤} {htG : rconj tG sG = tG ^ 2} {sH tH : H} {hgH : Subgroup.closure {sH, tH} = ⊤} {htH : rconj tH sH = tH ^ 2} (φ : G →* H) (hs : φ sG = sH) (ht : φ tG = tH) : tameSkeletalize G sG tG hgG htG ⟶ tameSkeletalize H sH tH hgH htH

A marking-preserving group hom φ : G →* H between two tame-marked groups induces a tame morphism of their skeletalizations. Stated with both G, H generic so the target skeleton MulOneClass is resolved (to groupFin) once in this generic context, never Fin.instMul.

Equations

• Q2Presentation.tameSkelHomBetween φ hs ht = Q2Presentation.tameSkeletalizeHomOut ((Q2Presentation.tameSkelEquiv H sH tH hgH htH).symm.toMonoidHom.comp φ) ⋯ ⋯

theorem Q2Presentation.tameSkelHomBetween_key {G : Type u_1} {H : Type u_2} [Group G] [Finite G] [Nonempty G] [Group H] [Finite H] [Nonempty H] {sG tG : G} {hgG : Subgroup.closure {sG, tG} = ⊤} {htG : rconj tG sG = tG ^ 2} {sH tH : H} {hgH : Subgroup.closure {sH, tH} = ⊤} {htH : rconj tH sH = tH ^ 2} (φ : G →* H) (hs : φ sG = sH) (ht : φ tG = tH) (y : Fin (tameSkeletalize G sG tG hgG htG).n) : (tameSkelEquiv H sH tH hgH htH) ((tameSkelHomBetween φ hs ht).toMonoidHom y) = φ ((tameSkelEquiv G sG tG hgG htG) y)

The induced morphism intertwines the transport equivalences with φ.

Nonemptiness: the trivial tame quotient

theorem Q2Presentation.tame_trivial_generates : Subgroup.closure {1, 1} = ⊤

theorem Q2Presentation.tame_trivial_tame : rconj 1 1 = 1 ^ 2

noncomputable def Q2Presentation.trivialTame : TameMarkedFinite

The trivial tame index (carrier Fin 1).

Equations

• Q2Presentation.trivialTame = Q2Presentation.tameSkeletalize Unit 1 1 Q2Presentation.tame_trivial_generates Q2Presentation.tame_trivial_tame

instance Q2Presentation.instNonemptyTameMarkedFinite : Nonempty TameMarkedFinite

Binary subdirect objects

def Q2Presentation.tameFamilySubgroup {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (s t : (i : ι) → G i) : Subgroup ((i : ι) → G i)

The subgroup of ∀ i, G i generated by the diagonal pair (s, t).

Equations

• Q2Presentation.tameFamilySubgroup s t = Subgroup.closure {s, t}

def Q2Presentation.tameFamilyS {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (s t : (i : ι) → G i) : ↥(tameFamilySubgroup s t)

The corestricted diagonal s.

Equations

• Q2Presentation.tameFamilyS s t = ⟨s, ⋯⟩

def Q2Presentation.tameFamilyT {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (s t : (i : ι) → G i) : ↥(tameFamilySubgroup s t)

The corestricted diagonal t.

Equations

• Q2Presentation.tameFamilyT s t = ⟨t, ⋯⟩

theorem Q2Presentation.tameFamily_generates {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (s t : (i : ι) → G i) : Subgroup.closure {tameFamilyS s t, tameFamilyT s t} = ⊤

theorem Q2Presentation.tameFamily_tame {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (s t : (i : ι) → G i) (h : ∀ (i : ι), rconj (t i) (s i) = t i ^ 2) : rconj (tameFamilyT s t) (tameFamilyS s t) = tameFamilyT s t ^ 2

def Q2Presentation.tameBinS (A B : TameMarkedFinite) (i : Fin 2) : Fin (![A, B] i).n

The s-component of the binary subdirect family of A, B.

Equations

• Q2Presentation.tameBinS A B i = (![A, B] i).s

def Q2Presentation.tameBinT (A B : TameMarkedFinite) (i : Fin 2) : Fin (![A, B] i).n

The t-component of the binary subdirect family of A, B.

Equations

• Q2Presentation.tameBinT A B i = (![A, B] i).t

noncomputable def Q2Presentation.tameSubdirectObj (A B : TameMarkedFinite) : TameMarkedFinite

The binary subdirect object of A, B: skeletalize the subgroup of Fin A.n × Fin B.n (as a Fin 2-product) generated by the diagonal (s, t), which satisfies the tame relation coordinatewise.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Q2Presentation.tameSubdirectFst (A B : TameMarkedFinite) : tameSubdirectObj A B ⟶ A

First projection of the binary subdirect object.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Q2Presentation.tameSubdirectSnd (A B : TameMarkedFinite) : tameSubdirectObj A B ⟶ B

Second projection of the binary subdirect object.

Equations

• One or more equations did not get rendered due to their size.

instance Q2Presentation.tameMarkedFinite_isCofiltered : CategoryTheory.IsCofiltered TameMarkedFinite

The tame index category is cofiltered.

The tame inverse system and its limit Ttame

noncomputable def Q2Presentation.tameDiagram : CategoryTheory.Functor TameMarkedFinite ProfiniteGrp.{0}

The inverse system of finite marked tame quotients, as a functor into ProfiniteGrp (mirrors admissibleDiagram).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Q2Presentation.tameDiagram_map_apply {A B : TameMarkedFinite} (f : A ⟶ B) (x : Fin A.n) : (ProfiniteGrp.Hom.hom (tameDiagram.map f)) x = f.toMonoidHom x

instance Q2Presentation.instFiniteTameObj (A : TameMarkedFinite) : Finite ↑(tameDiagram.obj A).toProfinite.toTop

noncomputable def Q2Presentation.Ttame : ProfiniteGrp.{0}

The profinite tame group T_A, the cofiltered inverse limit (in ProfiniteGrp) of all finite marked tame quotients (manuscript T_A, l.401).

Equations

• Q2Presentation.Ttame = CategoryTheory.Limits.limit Q2Presentation.tameDiagram

noncomputable def Q2Presentation.tameIso : Ttame ≅ ProfiniteGrp.limit tameDiagram

Bridge from the opaque categorical limit to mathlib's explicit subtype model.

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.tame_limit_pi_apply (A : TameMarkedFinite) (x : ↑Ttame.toProfinite.toTop) : (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π tameDiagram A)) x = ↑((ProfiniteGrp.Hom.hom tameIso.hom) x) A

The categorical projection Ttame ⟶ Fin A.n, via tameIso.

theorem Q2Presentation.Ttame_ext {x y : ↑Ttame.toProfinite.toTop} (h : ∀ (A : TameMarkedFinite), (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π tameDiagram A)) x = (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π tameDiagram A)) y) : x = y

Two points of Ttame agree once all coordinate projections agree.

The universal generators σ, τ

def Q2Presentation.tameGenSFamily : ↑(ProfiniteGrp.limit tameDiagram).toProfinite.toTop

The compatible family underlying σ: coordinate A.s at every A.

Equations

• Q2Presentation.tameGenSFamily = ⟨fun (A : Q2Presentation.TameMarkedFinite) => A.s, ⋯⟩

def Q2Presentation.tameGenTFamily : ↑(ProfiniteGrp.limit tameDiagram).toProfinite.toTop

The compatible family underlying τ: coordinate A.t at every A.

Equations

• Q2Presentation.tameGenTFamily = ⟨fun (A : Q2Presentation.TameMarkedFinite) => A.t, ⋯⟩

noncomputable def Q2Presentation.tameSigma : ↑Ttame.toProfinite.toTop

The universal generator σ of Ttame.

Equations

• Q2Presentation.tameSigma = (ProfiniteGrp.Hom.hom Q2Presentation.tameIso.inv) Q2Presentation.tameGenSFamily

noncomputable def Q2Presentation.tameTau : ↑Ttame.toProfinite.toTop

The universal generator τ of Ttame.

Equations

• Q2Presentation.tameTau = (ProfiniteGrp.Hom.hom Q2Presentation.tameIso.inv) Q2Presentation.tameGenTFamily

theorem Q2Presentation.tameSigma_eval (A : TameMarkedFinite) : (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π tameDiagram A)) tameSigma = A.s

Projecting σ to a coordinate returns A.s.

theorem Q2Presentation.tameTau_eval (A : TameMarkedFinite) : (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π tameDiagram A)) tameTau = A.t

Projecting τ to a coordinate returns A.t.

theorem Q2Presentation.Ttame_tameRel (A : TameMarkedFinite) : rconj ((ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π tameDiagram A)) tameTau) ((ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π tameDiagram A)) tameSigma) = (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π tameDiagram A)) tameTau ^ 2

The tame relation holds in Ttame (manuscript τ^σ = τ², l.401), in the inverse-limit sense: projecting the universal generators to any finite tame quotient A satisfies rconj τ σ = τ² there (because A is tame).

Topological generation

noncomputable def Q2Presentation.tameHomeo : ↑Ttame.toProfinite.toTop ≃ₜ ↑(ProfiniteGrp.limit tameDiagram).toProfinite.toTop

Ttame is homeomorphic to the explicit limit model via tameIso.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Q2Presentation.tameEvalAt (B : TameMarkedFinite) : ↑(ProfiniteGrp.limit tameDiagram).toProfinite.toTop →* ↑(tameDiagram.obj B).toProfinite.toTop

Evaluation at coordinate B, as a monoid hom out of the explicit limit.

Equations

• Q2Presentation.tameEvalAt B = { toFun := fun (m : ↑(ProfiniteGrp.limit Q2Presentation.tameDiagram).toProfinite.toTop) => ↑m B, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Q2Presentation.tameEvalAt_apply (B : TameMarkedFinite) (m : ↑(ProfiniteGrp.limit tameDiagram).toProfinite.toTop) : (tameEvalAt B) m = ↑m B

theorem Q2Presentation.map_tameEvalAt_closure_eq_top (B : TameMarkedFinite) : Subgroup.map (tameEvalAt B) (Subgroup.closure {tameGenSFamily, tameGenTFamily}) = ⊤

The coordinate-B evaluation maps the subgroup generated by σ, τ onto Fin B.n (its image is closure {B.s, B.t} = ⊤, by B.generates).

theorem Q2Presentation.tame_exists_dominating (J : Finset TameMarkedFinite) : ∃ (B : TameMarkedFinite), ∀ A ∈ J, Nonempty (B ⟶ A)

Finite cofiltered domination.

theorem Q2Presentation.dense_tameGenFamily : Dense ↑(Subgroup.closure {tameGenSFamily, tameGenTFamily})

The subgroup generated by σ, τ is dense in the explicit limit model.

theorem Q2Presentation.tameGen_topologically_generate : (Subgroup.closure {tameSigma, tameTau}).topologicalClosure = ⊤

The universal generators σ, τ topologically generate Ttame.

The unramified character nu_t : Ttame ⟶ ℤ₂

The unramified character sends σ to the topological generator 1 ∈ ℤ₂ and τ to 0 (τ is pro-odd, killed in the unramified pro-2 quotient — Lemma 3.1: every normal 2-subgroup of a finite tame quotient is central and unramified, so the only pro-2 data is the σ-direction). It is built as the map into the limit ℤ₂ = lim_n ZMod(2ⁿ) whose n-th layer is the projection of Ttame through the auxiliary cyclic-2-group tame quotient cyclicTame n (carrier C2Pow n, s = additive generator, t = 1). Compatibility across the layers is the reduction TameHom cyclicTame n ⟶ cyclicTame m together with the inverse-limit compatibility of Ttame.

theorem Q2Presentation.cyclicTame_gen (n : ℕ) : Subgroup.closure {Multiplicative.ofAdd 1, 1} = ⊤

The additive generator ofAdd 1 generates the cyclic 2-group C2Pow n.

theorem Q2Presentation.cyclicTame_tame (n : ℕ) : rconj 1 (Multiplicative.ofAdd 1) = 1 ^ 2

The tame relation holds trivially in C2Pow n (t = 1).

noncomputable def Q2Presentation.cyclicTame (n : ℕ) : TameMarkedFinite

The auxiliary cyclic 2-group tame quotient at layer n: carrier C2Pow n, s = additive generator, t = 1.

Equations

• Q2Presentation.cyclicTame n = Q2Presentation.tameSkeletalize (Q2Presentation.C2Pow n) (Multiplicative.ofAdd 1) 1 ⋯ ⋯

noncomputable def Q2Presentation.cyclicEquiv (n : ℕ) : Fin (cyclicTame n).n ≃* C2Pow n

The transport equivalence Fin (cyclicTame n).n ≃* C2Pow n.

Equations

• Q2Presentation.cyclicEquiv n = Q2Presentation.tameSkelEquiv (Q2Presentation.C2Pow n) (Multiplicative.ofAdd 1) 1 ⋯ ⋯

@[simp]

theorem Q2Presentation.cyclicEquiv_s (n : ℕ) : (cyclicEquiv n) (cyclicTame n).s = Multiplicative.ofAdd 1

@[simp]

theorem Q2Presentation.cyclicEquiv_t (n : ℕ) : (cyclicEquiv n) (cyclicTame n).t = 1

theorem Q2Presentation.castCMH_ofAdd_one {a b : ℕ} (h : 2 ^ a ∣ 2 ^ b) : (castCMH h) (Multiplicative.ofAdd 1) = Multiplicative.ofAdd 1

Reduction maps fix the additive generator ofAdd 1.

noncomputable def Q2Presentation.tameLayerHom (n : ℕ) : ↑Ttame.toProfinite.toTop →* C2Pow n

The n-th unramified layer hom Ttame →* C2Pow n: project to the auxiliary cyclic quotient cyclicTame n and read off the additive coordinate.

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.tameLayer_continuous (n : ℕ) : Continuous ⇑(tameLayerHom n)

noncomputable def Q2Presentation.redHom (n m : ℕ) (hmn : m ≤ n) : cyclicTame n ⟶ cyclicTame m

The reduction tame morphism cyclicTame n ⟶ cyclicTame m for m ≤ n, underlying the ℤ₂-layer maps ZMod(2ⁿ) → ZMod(2ᵐ).

Equations

• Q2Presentation.redHom n m hmn = Q2Presentation.tameSkelHomBetween (Q2Presentation.castCMH ⋯).toMonoidHom ⋯ ⋯

theorem Q2Presentation.redHom_key (n m : ℕ) (hmn : m ≤ n) (y : Fin (cyclicTame n).n) : (cyclicEquiv m) ((redHom n m hmn).toMonoidHom y) = (castCMH ⋯) ((cyclicEquiv n) y)

The reduction morphism intertwines the transport equivalences with the ℤ₂-layer reduction.

theorem Q2Presentation.tameLayer_compat (n m : ℕ) (hmn : m ≤ n) (x : ↑Ttame.toProfinite.toTop) : (castCMH ⋯) ((tameLayerHom n) x) = (tameLayerHom m) x

Layer compatibility: reducing the n-th layer to the m-th agrees with the m-th layer (m ≤ n). Uses the inverse-limit compatibility of Ttame through the reduction morphism redHom.

noncomputable def Q2Presentation.nu_t : Ttame ⟶ ProfiniteZ2

The unramified character ν_t : Ttame ⟶ ℤ₂, σ ↦ 1, τ ↦ 0. Built as the map into ℤ₂ = lim_n ZMod(2ⁿ) whose n-th coordinate is tameLayerHom n.

Equations

• One or more equations did not get rendered due to their size.

nu_t is the unramified character: σ ↦ 1, τ ↦ 0

theorem Q2Presentation.tameLayerHom_tameSigma (n : ℕ) : (tameLayerHom n) tameSigma = Multiplicative.ofAdd 1

theorem Q2Presentation.tameLayerHom_tameTau (n : ℕ) : (tameLayerHom n) tameTau = 1

theorem Q2Presentation.nu_t_tameSigma : (ProfiniteGrp.Hom.hom nu_t) tameSigma = z2One

ν_t sends σ to the topological generator 1 ∈ ℤ₂ (the unramified Frobenius coordinate).

theorem Q2Presentation.nu_t_tameTau : (ProfiniteGrp.Hom.hom nu_t) tameTau = z2Zero

ν_t sends τ to 0 ∈ ℤ₂ (τ is pro-odd, killed in the unramified pro-2 quotient — Lemma 3.1).