ClassFormation.cyclicFixedCycleEquiv
The actual fixed group A_K is the kernel of ρ(g)-1 on A_L when g generates G(L/K).
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]Lean source · full declaration
def cyclicFixedCycleEquiv
(A : Rep ℤ G)
(K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
(hnormal : (extensionSubgroup K L hLK).Normal)
(hfinite : Finite (K.toSubgroup ⧸ extensionSubgroup K L hLK))
(g : K.toSubgroup ⧸ extensionSubgroup K L hLK)
(hg : ∀ x, x ∈ Subgroup.zpowers g) :
letI := hnormal
letI := hfinite
letI := Fintype.ofFinite
(K.toSubgroup ⧸ extensionSubgroup K L hLK)
letI : IsCyclic
(K.toSubgroup ⧸ extensionSubgroup K L hLK) :=
isCyclic_of_generator g hg
letI : CommGroup
(K.toSubgroup ⧸ extensionSubgroup K L hLK) :=
IsCyclic.commGroup
let M := extensionFixedRepresentation A K L hLK hnormal
let T := Rep.FiniteCyclicGroup.normHomCompSub M g
ambientFixedAddSubgroup A K ≃+
T.moduleCatLeftHomologyData.K := by
dsimp only
letI := hnormal
letI := hfinite
letI := Fintype.ofFinite
(K.toSubgroup ⧸ extensionSubgroup K L hLK)
letI : IsCyclic (K.toSubgroup ⧸ extensionSubgroup K L hLK) :=
isCyclic_of_generator g hg
letI : CommGroup (K.toSubgroup ⧸ extensionSubgroup K L hLK) :=
IsCyclic.commGroup
let M := extensionFixedRepresentation A K L hLK hnormal
let T := Rep.FiniteCyclicGroup.normHomCompSub M g
let toCycle : ambientFixedAddSubgroup A K →
T.moduleCatLeftHomologyData.K := fun a => by
let aL := fixedFieldInclusion A K L hLK a
let aM : M.V :=
(extensionFixedRepresentationEquiv A K L hLK hnormal).symm aL
refine ⟨aM, sub_eq_zero.mpr ?_⟩
refine Quotient.inductionOn' g ?_
intro k
apply Subtype.ext
change A.ρ k.1 a.1 = a.1
exact a.2 k
let fromCycle : T.moduleCatLeftHomologyData.K →
ambientFixedAddSubgroup A K := fun x => by
let aM : M.V := x.1
let aL : ambientFixedAddSubgroup A L :=
extensionFixedRepresentationEquiv A K L hLK hnormal aM
have hxzero : T.g.hom aM = 0 := x.2
have hxg : M.ρ g aM = aM := by
apply sub_eq_zero.mp
exact hxzero
have hxall : ∀ q, M.ρ q aM = aM := by
let : Module ℤ M := M.hV2
exact (Representation.mem_invariants_iff_of_forall_mem_zpowers
M.ρ g hg aM).2 hxg
refine ⟨aL.1, ?_⟩
intro k
have hk := hxall
((QuotientGroup.mk' (extensionSubgroup K L hLK)) k)
have haction := extensionFixedRepresentation_action_coe
A K L hLK hnormal
((QuotientGroup.mk' (extensionSubgroup K L hLK)) k) aM
have haction' :
(M.ρ ((QuotientGroup.mk'
(extensionSubgroup K L hLK)) k) aM).1 =
A.ρ k.1 aL.1 := by
calc
_ = relativeCosetAction A K L hLK aL
((QuotientGroup.mk'
(extensionSubgroup K L hLK)) k) := haction
_ = A.ρ k.1 aL.1 :=
relativeCosetAction_mk A K L hLK aL k
exact haction'.symm.trans ((congrArg Subtype.val hk).trans rfl)
exact
{ toFun := toCycle
invFun := fromCycle
left_inv := by
intro a
apply Subtype.ext
rfl
right_inv := by
intro x
apply Subtype.ext
rfl
map_add' := by
intro a b
apply Subtype.ext
apply Subtype.ext
rfl }