RestrictedFinite.lean

def restrictedNthPowersSubgroup
    (n : ℕ+) (Delta : KummerSubgroup K n) : Subgroup Delta.1

theorem mem_restrictedNthPowersSubgroup_iff
    (n : ℕ+) (Delta : KummerSubgroup K n) {a : Delta.1} :
    a ∈ restrictedNthPowersSubgroup n Delta ↔
      ∃ b : Kˣ, b ^ (n : ℕ) = a.1

def RestrictedRadicalQuotient
    (n : ℕ+) (Delta : KummerSubgroup K n)

instance restrictedRadicalQuotient_commGroupInstance
    (n : ℕ+) (Delta : KummerSubgroup K n) :
    CommGroup (RestrictedRadicalQuotient n Delta)

def restrictedRadicalQuotientMulEquiv
    (n : ℕ+) (Delta : KummerSubgroup K n) :
    RestrictedRadicalQuotient n Delta ≃*
      (Delta.1 ⧸ restrictedNthPowersSubgroup n Delta)

def restrictedRadicalQuotientMk
    (n : ℕ+) (Delta : KummerSubgroup K n) :
    Delta.1 →* RestrictedRadicalQuotient n Delta

theorem restrictedRadicalQuotientMk_eq_one_iff
    (n : ℕ+) (Delta : KummerSubgroup K n) (a : Delta.1) :
    restrictedRadicalQuotientMk n Delta a = 1 ↔
      a ∈ restrictedNthPowersSubgroup n Delta

theorem restrictedRadicalQuotientMk_eq_iff
    (n : ℕ+) (Delta : KummerSubgroup K n) (a b : Delta.1) :
    restrictedRadicalQuotientMk n Delta a =
        restrictedRadicalQuotientMk n Delta b ↔
      a / b ∈ restrictedNthPowersSubgroup n Delta

theorem restrictedRadicalQuotientMk_surjective
    (n : ℕ+) (Delta : KummerSubgroup K n) :
    Function.Surjective (restrictedRadicalQuotientMk n Delta)

theorem restrictedRadicalQuotient_inductionOn
    (n : ℕ+) (Delta : KummerSubgroup K n)
    {motive : RestrictedRadicalQuotient n Delta → Prop}
    (q : RestrictedRadicalQuotient n Delta)
    (mk : ∀ a : Delta.1,
      motive (restrictedRadicalQuotientMk n Delta a)) :
    motive q

def restrictedRadicalQuotientLift {M : Type*} [Group M]
    (n : ℕ+) (Delta : KummerSubgroup K n) (f : Delta.1 →* M)
    (hf : restrictedNthPowersSubgroup n Delta ≤ MonoidHom.ker f) :
    RestrictedRadicalQuotient n Delta →* M

theorem restrictedRadicalQuotientLift_mk {M : Type*} [Group M]
    (n : ℕ+) (Delta : KummerSubgroup K n) (f : Delta.1 →* M)
    (hf : restrictedNthPowersSubgroup n Delta ≤ MonoidHom.ker f)
    (a : Delta.1) :
    restrictedRadicalQuotientLift n Delta f hf
        (restrictedRadicalQuotientMk n Delta a) = f a

theorem restrictedKummerFixed
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    ∀ sigma : Gal(L/K), ∀ u : Lˣ,
      u ^ (n : ℕ) = 1 → sigma • u = u

def restrictedRadicalInclusion
    (n : ℕ+) (Delta : KummerSubgroup K n)
    (hDelta : Delta.1 ≤ finiteKummerRadicalSubgroup (K := K) (L := L) n) :
    Delta.1 →* (chosenFiniteKummerRadicalDatum (K := K) (L := L) n).carrier

def restrictedSubgroupKummerCharacter
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n)
    (hDelta : Delta.1 ≤ finiteKummerRadicalSubgroup (K := K) (L := L) n) :
    Delta.1 →* (Gal(L/K) →* nthRootsSubgroup L (n : ℕ))

theorem ker_restrictedSubgroupKummerCharacter
    [IsGalois K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n)
    (hDelta : Delta.1 ≤ finiteKummerRadicalSubgroup (K := K) (L := L) n) :
    MonoidHom.ker (restrictedSubgroupKummerCharacter n hmu Delta hDelta) =
      restrictedNthPowersSubgroup n Delta

def restrictedQuotientKummerCharacter
    [IsGalois K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n)
    (hDelta : Delta.1 ≤ finiteKummerRadicalSubgroup (K := K) (L := L) n) :
    RestrictedRadicalQuotient n Delta →*
      (Gal(L/K) →* nthRootsSubgroup L (n : ℕ))

theorem restrictedQuotientKummerCharacter_mk
    [IsGalois K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n)
    (hDelta : Delta.1 ≤ finiteKummerRadicalSubgroup (K := K) (L := L) n)
    (a : Delta.1) :
    restrictedQuotientKummerCharacter n hmu Delta hDelta
        (restrictedRadicalQuotientMk n Delta a) =
      restrictedSubgroupKummerCharacter n hmu Delta hDelta a

theorem restrictedQuotientKummerCharacter_injective
    [IsGalois K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n)
    (hDelta : Delta.1 ≤ finiteKummerRadicalSubgroup (K := K) (L := L) n) :
    Function.Injective (restrictedQuotientKummerCharacter n hmu Delta hDelta)

def restrictedKummerTranspose
    [IsGalois K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n)
    (hDelta : Delta.1 ≤ finiteKummerRadicalSubgroup (K := K) (L := L) n) :
    Gal(L/K) →*
      (RestrictedRadicalQuotient n Delta →* nthRootsSubgroup L (n : ℕ)) where
  toFun sigma :=
    { toFun := fun q => restrictedQuotientKummerCharacter n hmu Delta hDelta q sigma
      map_one' := by simp
      map_mul' := by
        intro q r
        exact congrArg (fun chi : Gal(L/K) →* nthRootsSubgroup L (n : ℕ) => chi sigma)
          (map_mul (restrictedQuotientKummerCharacter n hmu Delta hDelta) q r) }
  map_one' := by
    apply MonoidHom.ext
    intro q
    exact map_one (restrictedQuotientKummerCharacter n hmu Delta hDelta q)
  map_mul' := by
    intro sigma tau
    apply MonoidHom.ext
    intro q
    exact map_mul (restrictedQuotientKummerCharacter n hmu Delta hDelta q) sigma tau

theorem restrictedKummerTranspose_apply
    [IsGalois K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n)
    (hDelta : Delta.1 ≤ finiteKummerRadicalSubgroup (K := K) (L := L) n)
    (sigma : Gal(L/K)) (q : RestrictedRadicalQuotient n Delta) :
    restrictedKummerTranspose n hmu Delta hDelta sigma q =
      restrictedQuotientKummerCharacter n hmu Delta hDelta q sigma

theorem restrictedKummerTranspose_fixes_root
    [IsGalois K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n)
    (hDelta : Delta.1 ≤ finiteKummerRadicalSubgroup (K := K) (L := L) n)
    (sigma : Gal(L/K))
    (hsigma : restrictedKummerTranspose n hmu Delta hDelta sigma = 1)
    {beta : L}
    (hbeta : beta ∈ kummerRootSet (K := K) (Omega := L) n Delta.1) :
    sigma beta = beta

theorem restrictedKummerTranspose_injective_of_adjoin
    [IsGalois K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n)
    (hDelta : Delta.1 ≤ finiteKummerRadicalSubgroup (K := K) (L := L) n)
    (hgenerate : IntermediateField.adjoin K
      (kummerRootSet (K := K) (Omega := L) n Delta.1) = ⊤) :
    Function.Injective (restrictedKummerTranspose n hmu Delta hDelta)

theorem restrictedRadicalQuotient_pow_eq_one
    (n : ℕ+) (Delta : KummerSubgroup K n)
    (q : RestrictedRadicalQuotient n Delta) :
    q ^ (n : ℕ) = 1

theorem restrictedQuotientKummerCharacter_surjective_of_adjoin
    [FiniteDimensional K L] [IsGalois K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n)
    (hDelta : Delta.1 ≤ finiteKummerRadicalSubgroup (K := K) (L := L) n)
    (hgenerate : IntermediateField.adjoin K
      (kummerRootSet (K := K) (Omega := L) n Delta.1) = ⊤) :
    Function.Surjective (restrictedQuotientKummerCharacter n hmu Delta hDelta)

def restrictedKummerCharacterMulEquivOfAdjoin
    [FiniteDimensional K L] [IsGalois K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n)
    (hDelta : Delta.1 ≤ finiteKummerRadicalSubgroup (K := K) (L := L) n)
    (hgenerate : IntermediateField.adjoin K
      (kummerRootSet (K := K) (Omega := L) n Delta.1) = ⊤) :
    RestrictedRadicalQuotient n Delta ≃*
      (Gal(L/K) →* nthRootsSubgroup L (n : ℕ))

theorem finiteKummerRadicalSubgroup_eq_of_adjoin
    [FiniteDimensional K L] [IsGalois K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n)
    (hDelta : Delta.1 ≤ finiteKummerRadicalSubgroup (K := K) (L := L) n)
    (hgenerate : IntermediateField.adjoin K
      (kummerRootSet (K := K) (Omega := L) n Delta.1) = ⊤) :
    finiteKummerRadicalSubgroup (K := K) (L := L) n = Delta.1