Cyclotomic ℤₚ-extension

The field $K(\mu_{p^\infty})$

def CyclotomicPinfField (p : ℕ) (K : Type u_1) [Field K] : Type u_1

The field $K(\mu_{p^\infty})$. Internally it is defined to be an IntermediateField K (SeparableClosure K), but please avoid using it in the public interface. Instead, use IsSepClosed.lift to construct a map of it to SeparableClosure K.

Equations

• CyclotomicPinfField p K = ↥(IntermediateField.adjoin K {x : SeparableClosure K | ∃ (n : ℕ), x ^ p ^ n = 1})

noncomputable instance CyclotomicPinfField.instField (p : ℕ) (K : Type u_1) [Field K] : Field (CyclotomicPinfField p K)

Equations

• CyclotomicPinfField.instField p K = inferInstanceAs (Field ↥(IntermediateField.adjoin K {x : SeparableClosure K | ∃ (n : ℕ), x ^ p ^ n = 1}))

noncomputable instance CyclotomicPinfField.algebra (p : ℕ) (K : Type u_1) [Field K] : Algebra K (CyclotomicPinfField p K)

Equations

• CyclotomicPinfField.algebra p K = inferInstanceAs (Algebra K ↥(IntermediateField.adjoin K {x : SeparableClosure K | ∃ (n : ℕ), x ^ p ^ n = 1}))

noncomputable instance CyclotomicPinfField.instInhabited (p : ℕ) (K : Type u_1) [Field K] : Inhabited (CyclotomicPinfField p K)

Equations

• CyclotomicPinfField.instInhabited p K = { default := 0 }

instance CyclotomicPinfField.instCharZero (p : ℕ) (K : Type u_1) [Field K] [CharZero K] : CharZero (CyclotomicPinfField p K)

instance CyclotomicPinfField.instCharP (p : ℕ) (K : Type u_1) [Field K] (p' : ℕ) [CharP K p'] : CharP (CyclotomicPinfField p K) p'

instance CyclotomicPinfField.instExpChar (p : ℕ) (K : Type u_1) [Field K] (p' : ℕ) [ExpChar K p'] : ExpChar (CyclotomicPinfField p K) p'

noncomputable instance CyclotomicPinfField.algebra' (p : ℕ) (K : Type u_1) [Field K] (R : Type u_2) [CommRing R] [Algebra R K] : Algebra R (CyclotomicPinfField p K)

Equations

• CyclotomicPinfField.algebra' p K R = inferInstanceAs (Algebra R ↥(IntermediateField.adjoin K {x : SeparableClosure K | ∃ (n : ℕ), x ^ p ^ n = 1}))

instance CyclotomicPinfField.instIsScalarTower (p : ℕ) (K : Type u_1) [Field K] (R : Type u_2) [CommRing R] [Algebra R K] : IsScalarTower R K (CyclotomicPinfField p K)

instance CyclotomicPinfField.instNoZeroSMulDivisors (p : ℕ) (K : Type u_1) [Field K] (R : Type u_2) [CommRing R] [Algebra R K] [IsFractionRing R K] : NoZeroSMulDivisors R (CyclotomicPinfField p K)

instance CyclotomicPinfField.isSeparable (p : ℕ) (K : Type u_1) [Field K] : Algebra.IsSeparable K (CyclotomicPinfField p K)

theorem CyclotomicPinfField.isCyclotomicExtension' (p : ℕ) (K : Type u_1) [Field K] [NeZero ↑p] (s : Set ℕ) (h1 : s ⊆ {0} ∪ Set.range fun (x : ℕ) => p ^ x) (h2 : ∀ (N : ℕ), ∃ n ≥ N, p ^ n ∈ s) : IsCyclotomicExtension s K (CyclotomicPinfField p K)

instance CyclotomicPinfField.isCyclotomicExtension (p : ℕ) (K : Type u_1) [Field K] [NeZero ↑p] : IsCyclotomicExtension (Set.range fun (x : ℕ) => p ^ x) K (CyclotomicPinfField p K)

instance CyclotomicPinfField.hasEnoughRootsOfUnity (p : ℕ) (K : Type u_1) [Field K] [NeZero ↑p] (i : ℕ) : HasEnoughRootsOfUnity (CyclotomicPinfField p K) (p ^ i)

Some complemenatry results on cyclotomic character

noncomputable def continuousCyclotomicCharacter (p : ℕ) (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] [Fact (Nat.Prime p)] : (L ≃ₐ[K] L) →ₜ* ℤ_[p]ˣ

The restriction of cyclotomicCharacter to L ≃ₐ[K] L and which is continuous.

Equations

• continuousCyclotomicCharacter p K L = { toMonoidHom := (cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut (L ≃ₐ[K] L) L), continuous_toFun := ⋯ }

@[simp]

theorem continuousCyclotomicCharacter_toMonoidHom (p : ℕ) (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] [Fact (Nat.Prime p)] : (continuousCyclotomicCharacter p K L).toMonoidHom = (cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut (L ≃ₐ[K] L) L)

@[simp]

theorem continuousCyclotomicCharacter_apply (p : ℕ) (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] [Fact (Nat.Prime p)] (f : L ≃ₐ[K] L) : (continuousCyclotomicCharacter p K L) f = (cyclotomicCharacter L p) ↑f

theorem isClosed_ker_continuousCyclotomicCharacter (p : ℕ) (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] [Fact (Nat.Prime p)] : IsClosed ↑(continuousCyclotomicCharacter p K L).ker

theorem IntermediateField.adjoin_le_fixedField_ker_continuousCyclotomicCharacter (p : ℕ) (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] [Fact (Nat.Prime p)] [∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)] : adjoin K {x : L | ∃ (n : ℕ), x ^ p ^ n = 1} ≤ fixedField (continuousCyclotomicCharacter p K L).ker

theorem IntermediateField.adjoin_eq_fixedField_ker_continuousCyclotomicCharacter (p : ℕ) (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] [Fact (Nat.Prime p)] [∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)] [IsGalois K L] : adjoin K {x : L | ∃ (n : ℕ), x ^ p ^ n = 1} = fixedField (continuousCyclotomicCharacter p K L).ker