RayClassSubgroupPrimeArtin.lean

theorem arithmeticFinitePlacePrimeArtin_restrict_tower
    (K L E : Type) [Field K] [Field L] [Field E]
    [NumberField K] [NumberField L] [NumberField E]
    [Algebra K L] [Algebra K E] [Algebra E L] [IsScalarTower K E L]
    [IsAbelianGalois K L] [IsAbelianGalois K E]
    (v : HeightOneSpectrum (𝓞 K)) :
    AlgEquiv.restrictNormalHom E
        (arithmeticFinitePlacePrimeArtin (K := K) (L := L) v) =
      arithmeticFinitePlacePrimeArtin (K := K) (L := E) v

theorem rayClassFieldGaloisEquivRayClassGroup_symm_mk
    {K : Type} [Field K] [NumberField K]
    (m : RayClass.Modulus K) (c : IdeleClassGroup K) :
    (rayClassFieldGaloisEquivRayClassGroup (K := K) m).symm
        (QuotientGroup.mk' m.congruenceSubgroup c) =
      globalNormResidueMonoidHom K (rayClassField K m) c

theorem rayClassField_arithmeticFinitePlacePrimeArtin
    {K : Type} [Field K] [NumberField K]
    (m : RayClass.Modulus K)
    (v : HeightOneSpectrum (𝓞 K)) :
    (rayClassFieldGaloisEquivRayClassGroup (K := K) m).symm
        ((QuotientGroup.mk' m.congruenceSubgroup
          (QuotientGroup.mk' (IdeleGroup.principalSubgroup K)
            (IdeleGroup.finitePrimeIdele v)))⁻¹) =
      arithmeticFinitePlacePrimeArtin (K := K) (L := rayClassField K m) v

theorem rayClassSubgroup_restrict_transport
    {K : Type} [Field K] [NumberField K]
    (m : RayClass.Modulus K)
    (H : Subgroup (RayClass.RayClassGroup m))
    (σ : rayClassField K m ≃ₐ[K] rayClassField K m) :
    let F := rayClassSubgroupFixedField (K := K) m H
    let E := rayClassSubgroupSubextension (K := K) m H
    let α : F ≃ₐ[K] E :=
      IntermediateField.equivMap F (rayClassFieldEmbedding K m)
    let f : E →ₐ[K] rayClassField K m :=
      (IntermediateField.val F).comp α.symm.toAlgHom
    let _ : Algebra E (rayClassField K m) := f.toRingHom.toAlgebra
    let _ : IsScalarTower K E (rayClassField K m) :=
      IsScalarTower.of_algebraMap_eq fun x => (f.commutes x).symm
    (AlgEquiv.autCongr α) (AlgEquiv.restrictNormalHom F σ) =
      AlgEquiv.restrictNormalHom E σ := by
  let F := rayClassSubgroupFixedField (K := K) m H
  let L := rayClassField K m
  let E := rayClassSubgroupSubextension (K := K) m H
  let α : F ≃ₐ[K] E :=
    IntermediateField.equivMap F (rayClassFieldEmbedding K m)
  let f : E →ₐ[K] L :=
    (IntermediateField.val F).comp α.symm.toAlgHom
  let : Algebra E L := f.toRingHom.toAlgebra
  let : IsScalarTower K E L :=
    IsScalarTower.of_algebraMap_eq fun x => (f.commutes x).symm
  change (AlgEquiv.autCongr α) (AlgEquiv.restrictNormalHom F σ) =
    AlgEquiv.restrictNormalHom E σ
  apply AlgEquiv.ext
  intro x
  apply f.injective
  change f (α ((AlgEquiv.restrictNormalHom F σ) (α.symm x))) =
    f ((AlgEquiv.restrictNormalHom E σ) x)
  calc
    f (α ((AlgEquiv.restrictNormalHom F σ) (α.symm x))) =
        F.val ((AlgEquiv.restrictNormalHom F σ) (α.symm x)) := by
          simp [f]
    _ = σ (F.val (α.symm x)) :=
      AlgEquiv.restrictNormalHom_apply F σ (α.symm x)
    _ = f ((AlgEquiv.restrictNormalHom E σ) x) := by
      exact (AlgEquiv.restrictNormal_commutes σ E x).symm

theorem rayClassSubgroupArtin_finitePrimeIdele
    {K : Type} [Field K] [NumberField K]
    (m : RayClass.Modulus K)
    (H : Subgroup (RayClass.RayClassGroup m))
    (v : HeightOneSpectrum (𝓞 K)) :
    rayClassSubgroupArtin (K := K) m H
        (QuotientGroup.mk' m.congruenceSubgroup
          (QuotientGroup.mk' (IdeleGroup.principalSubgroup K)
            (IdeleGroup.finitePrimeIdele v))) =
      arithmeticFinitePlacePrimeArtin (K := K)
        (L := rayClassSubgroupSubextension (K := K) m H) v