ClassFieldTower.Martinet.Shafarevich.trivial_relativeH1Action_fixes_primePower_roots
An upper automorphism fixing the lower cyclotomic field fixes every root at the selected prime-power level if its restriction acts trivially on the lower H¹. The logarithmic minimum is constructed inside the proof.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
-- Six Algebra structures (including the canonical K-algebra E), two towers,
-- and five fields give thirteen data structures. The proof adds only two
-- finite-dimensionality propositions and ordinary bundled valuation data.Lean source · statement
theorem trivial_relativeH1Action_fixes_primePower_roots
{F K L Ω : Type*} [Field F] [Field K] [Field L] [Field Ω]
[Algebra F K] [Algebra K Ω] [IsAlgClosure K Ω] [CharZero K]
(E : IntermediateField K Ω)
[Algebra F L] [Algebra F E] [Algebra L E]
[IsScalarTower F K E] [IsScalarTower F L E]
[FiniteDimensional F K] [Normal F K]
(vF : _root_.Valuation F (WithZero (Multiplicative ℤ)))
(vE : _root_.Valuation E (WithZero (Multiplicative ℤ)))
[ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete vF]
[ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete vE]
[vF.HasExtension vE]
(p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField vE.valuationSubring) p]
[IsCyclotomicExtension {p} F L] [IsCyclotomicExtension {p} K E]
(s : ℕ) (hmu : (primitiveRoots (p ^ (s + 1)) E).Nonempty)
(τupper : Gal(E/L))
(hτ : relativeGaloisH1Action (n := p ^ (s + 1)) F K
(IntermediateField.restrictRestrictAlgEquivMapHom F K L E τupper) = 1) :
∀ ζ : E, ζ ^ (p ^ (s + 1)) = 1 → τupper ζ = ζ