OAI/NumberTheory/DukePrimeDegree/Arithmetic/FixedFieldTower.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The cyclic fixed-field tower

The automorphisms over a fixed field are the original subgroup. Passing to a smaller subgroup in this cyclic extension preserves the actual underlying intermediate field, so the cyclic factorization applies to the same fixed-field zeta orders used by descent.

  1. lemma OAI.DukePrimeDegree.subgroupEquivAlgEquiv_apply line 21
  2. lemma OAI.DukePrimeDegree.fixingSubgroup_extendScalars_fixedField line 24
  3. lemma OAI.DukePrimeDegree.zpowers_comap_subtype line 45
  4. lemma OAI.DukePrimeDegree.fixingSubgroup_extendScalars_zpowers line 52