CyclotomicZHatBaseChange.lean

instance rationalSeparableClosure_isGalois :
    IsGalois ℚ (SeparableClosure ℚ)

instance rationalSeparableClosure_isNormal :
    Normal ℚ (SeparableClosure ℚ)

def rationalCyclotomicZHatField :
    IntermediateField ℚ (SeparableClosure ℚ)

instance rationalCyclotomicZHatField_isAbelianGalois :
    IsAbelianGalois ℚ rationalCyclotomicZHatField

theorem rationalCyclotomicZHatField_normal :
    @Normal ℚ rationalCyclotomicZHatField _ _
      rationalCyclotomicZHatField.algebra'

instance rationalCyclotomicZHatField_isNormal :
    Normal ℚ rationalCyclotomicZHatField

def rationalCyclotomicZHatFieldGalEquivZHat :
    (rationalCyclotomicZHatField ≃ₐ[ℚ]
      rationalCyclotomicZHatField) ≃ₜ*
        Multiplicative ZHat

def rationalCyclotomicFullRestrictionToZHat :
    (KummerTheory.rationalCyclotomicField ≃ₐ[ℚ]
        KummerTheory.rationalCyclotomicField) →*
      (rationalCyclotomicZHatField ≃ₐ[ℚ]
        rationalCyclotomicZHatField)

theorem rationalCyclotomicZHatFieldGalEquivZHat_fullRestriction
    (σ :
      KummerTheory.rationalCyclotomicField ≃ₐ[ℚ]
        KummerTheory.rationalCyclotomicField) :
    rationalCyclotomicZHatFieldGalEquivZHat
        (rationalCyclotomicFullRestrictionToZHat σ) =
      (KummerTheory.zHatUnitsDecomposition
        (KummerTheory.rationalCyclotomicCharacterContinuousMulEquiv
          σ)).1

def
    rationalAbsoluteGaloisRestrictionToCyclotomicZHat :
    (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ) →ₜ*
      (rationalCyclotomicZHatField ≃ₐ[ℚ]
        rationalCyclotomicZHatField) where
  toMonoidHom :=
    @AlgEquiv.restrictNormalHom
      ℚ _ (SeparableClosure ℚ) _ _
      rationalCyclotomicZHatField _
      rationalCyclotomicZHatField.algebra' _ _
      rationalCyclotomicZHatField_normal
  continuous_toFun := by
    let : @Normal ℚ rationalCyclotomicZHatField _ _
        rationalCyclotomicZHatField.algebra' :=
      rationalCyclotomicZHatField_normal
    exact
      InfiniteGalois.restrictNormalHom_continuous
        rationalCyclotomicZHatField

def rationalCyclotomicDegreeData :
    DegreeData
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ) where
  degree :=
    (ContinuousMonoidHom.toContinuousMonoidHom
      rationalCyclotomicZHatFieldGalEquivZHat).comp
        rationalAbsoluteGaloisRestrictionToCyclotomicZHat
  degree_surjective :=
    by
      let : @Normal ℚ rationalCyclotomicZHatField _ _
          rationalCyclotomicZHatField.algebra' :=
        rationalCyclotomicZHatField_normal
      exact
        rationalCyclotomicZHatFieldGalEquivZHat.surjective.comp
          (AlgEquiv.restrictNormalHom_surjective
            (F := ℚ)
            (K₁ := rationalCyclotomicZHatField)
            (E := SeparableClosure ℚ))

theorem rationalCyclotomicDegreeData_inertia :
    rationalCyclotomicDegreeData.inertia =
      RamificationTheory.closedFixingSubgroup ℚ (SeparableClosure ℚ)
        rationalCyclotomicZHatField

theorem rationalCyclotomicDegreeData_fixedField_inertia :
    LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ)
        rationalCyclotomicDegreeData.inertia =
      rationalCyclotomicZHatField

theorem
    rationalCyclotomicDegreeData_fixedField_fieldInertia
    (H : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ)
        (rationalCyclotomicDegreeData.fieldInertia H) =
      LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H ⊔
        rationalCyclotomicZHatField

theorem
    rationalAbsoluteGaloisRestriction_image_eq_intersection_fixingSubgroup
    (H : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    H.toSubgroup.map
        rationalAbsoluteGaloisRestrictionToCyclotomicZHat.toMonoidHom =
      (((LocalClassFieldTheory.abstractFixedField
            ℚ (SeparableClosure ℚ) H) ⊓
        rationalCyclotomicZHatField).restrict
        (show
          LocalClassFieldTheory.abstractFixedField
                ℚ (SeparableClosure ℚ) H ⊓
              rationalCyclotomicZHatField ≤
            rationalCyclotomicZHatField from
          inf_le_right)).fixingSubgroup := by
  let _ : T2Space
      (rationalCyclotomicZHatField ≃ₐ[ℚ]
        rationalCyclotomicZHatField) :=
    krullTopology_t2
  let r := rationalAbsoluteGaloisRestrictionToCyclotomicZHat
  let R : ClosedSubgroup
      (rationalCyclotomicZHatField ≃ₐ[ℚ]
        rationalCyclotomicZHatField) :=
    { toSubgroup := H.toSubgroup.map r
      isClosed' := by
        change IsClosed (r '' H.carrier)
        exact
          (H.isClosed'.isCompact.image
            r.continuous).isClosed }
  let F :=
    LocalClassFieldTheory.abstractFixedField
      ℚ (SeparableClosure ℚ) H
  let J : IntermediateField ℚ (SeparableClosure ℚ) :=
    F ⊓ rationalCyclotomicZHatField
  let hJT : J ≤ rationalCyclotomicZHatField :=
    inf_le_right
  let E : IntermediateField ℚ rationalCyclotomicZHatField :=
    J.restrict hJT
  have hE :
      E = IntermediateField.fixedField R.toSubgroup := by
    apply
      (IntermediateField.lift_injective
        rationalCyclotomicZHatField)
    calc
      IntermediateField.lift E = J :=
        IntermediateField.lift_restrict hJT
      _ =
          IntermediateField.lift
            (IntermediateField.fixedField R.toSubgroup) := by
        dsimp only [F, J, R, r]
        change
          IntermediateField.fixedField H.toSubgroup ⊓
              rationalCyclotomicZHatField =
            IntermediateField.lift
              (IntermediateField.fixedField
                (Subgroup.map
                  (@AlgEquiv.restrictNormalHom
                    ℚ _ (SeparableClosure ℚ) _ _
                    rationalCyclotomicZHatField _
                    rationalCyclotomicZHatField.algebra' _ _
                    rationalCyclotomicZHatField_normal)
                  H.toSubgroup))
        exact
          @InfiniteGalois.restrict_fixedField
            ℚ (SeparableClosure ℚ) _ _ _ H.toSubgroup
            rationalCyclotomicZHatField
            rationalCyclotomicZHatField_normal
  have hfix :
      E.fixingSubgroup = R.toSubgroup := by
    rw [hE]
    exact InfiniteGalois.fixingSubgroup_fixedField R
  exact hfix.symm

theorem
    rationalCyclotomicDegreeData_fieldImage_eq_intersection_fixingSubgroup :
    ∀ H : ClosedSubgroup
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ),
      rationalCyclotomicDegreeData.fieldImage H =
        (((LocalClassFieldTheory.abstractFixedField
              ℚ (SeparableClosure ℚ) H) ⊓
            rationalCyclotomicZHatField).restrict
          (show
            LocalClassFieldTheory.abstractFixedField
                  ℚ (SeparableClosure ℚ) H ⊓
                rationalCyclotomicZHatField ≤
              rationalCyclotomicZHatField from
            inf_le_right)).fixingSubgroup.map
              rationalCyclotomicZHatFieldGalEquivZHat.toMonoidHom := by
  intro H
  rw [rationalCyclotomicDegreeData.fieldImage_eq_map]
  change
    H.toSubgroup.map
        (rationalCyclotomicZHatFieldGalEquivZHat.toMonoidHom.comp
          rationalAbsoluteGaloisRestrictionToCyclotomicZHat.toMonoidHom) =
      (((LocalClassFieldTheory.abstractFixedField
            ℚ (SeparableClosure ℚ) H) ⊓
          rationalCyclotomicZHatField).restrict
        (show
          LocalClassFieldTheory.abstractFixedField
                ℚ (SeparableClosure ℚ) H ⊓
              rationalCyclotomicZHatField ≤
            rationalCyclotomicZHatField from
          inf_le_right)).fixingSubgroup.map
        rationalCyclotomicZHatFieldGalEquivZHat.toMonoidHom
  rw [← Subgroup.map_map,
    rationalAbsoluteGaloisRestriction_image_eq_intersection_fixingSubgroup]

theorem
    rationalCyclotomicDegreeData_residueDegree_eq_intersection_finrank
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    (H.residueDegree rationalCyclotomicDegreeData : ℕ) =
      Module.finrank ℚ
        ((LocalClassFieldTheory.abstractFixedField
            ℚ (SeparableClosure ℚ) H.field ⊓
          rationalCyclotomicZHatField :
            IntermediateField ℚ (SeparableClosure ℚ)))

theorem
    abstractFixedFieldCyclotomicZHatIntersection_finrank_eq_of_embedding
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (ι :
      LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field →ₐ[ℚ]
        SeparableClosure ℚ) :
    Module.finrank ℚ
        ((ι.fieldRange ⊓ rationalCyclotomicZHatField :
          IntermediateField ℚ (SeparableClosure ℚ))) =
      Module.finrank ℚ
        ((LocalClassFieldTheory.abstractFixedField
            ℚ (SeparableClosure ℚ) H.field ⊓
          rationalCyclotomicZHatField :
            IntermediateField ℚ (SeparableClosure ℚ)))

instance rationalCyclotomicZHatFieldGal_isMulTorsionFree :
    IsMulTorsionFree
      (rationalCyclotomicZHatField ≃ₐ[ℚ]
        rationalCyclotomicZHatField)

def numberFieldCyclotomicZHatIntersection :
    IntermediateField ℚ (SeparableClosure ℚ)

def numberFieldCyclotomicZHatIntersectionEmbedding :
    numberFieldCyclotomicZHatIntersection K →ₐ[ℚ] K

theorem numberFieldCyclotomicZHatIntersectionEmbedding_commutes
    (x : numberFieldCyclotomicZHatIntersection K) :
    numberFieldSeparableClosureEmbedding K
        (numberFieldCyclotomicZHatIntersectionEmbedding K x) =
      (x : SeparableClosure ℚ)

instance
    numberFieldCyclotomicZHatIntersection_finiteDimensional :
    FiniteDimensional ℚ
      (numberFieldCyclotomicZHatIntersection K)

instance
    numberFieldCyclotomicZHatIntersection_numberField :
    NumberField (numberFieldCyclotomicZHatIntersection K) where
  to_charZero := inferInstance
  to_finiteDimensional := inferInstance

instance
    numberFieldCyclotomicZHatIntersection_isAbelianGalois :
    IsAbelianGalois ℚ
      (numberFieldCyclotomicZHatIntersection K)

def cyclotomicZHatIntersectionDegree : ℕ

theorem
    cyclotomicZHatIntersectionDegree_abstractFixedField_eq_intersection_finrank
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    let F :=
      LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field
    letI : FiniteDimensional ℚ F :=
      LocalClassFieldTheory.abstractFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ) H.field H.finite
    letI : NumberField F :=
      NumberField.of_module_finite ℚ F
    cyclotomicZHatIntersectionDegree F =
      Module.finrank ℚ
        ((F ⊓ rationalCyclotomicZHatField :
          IntermediateField ℚ (SeparableClosure ℚ))) := by
  dsimp only
  let F :=
    LocalClassFieldTheory.abstractFixedField
      ℚ (SeparableClosure ℚ) H.field
  let : FiniteDimensional ℚ F :=
    LocalClassFieldTheory.abstractFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) H.field H.finite
  let : NumberField F :=
    NumberField.of_module_finite ℚ F
  change
    Module.finrank ℚ
        (numberFieldCyclotomicZHatIntersection F) =
      Module.finrank ℚ
        ((F ⊓ rationalCyclotomicZHatField :
          IntermediateField ℚ (SeparableClosure ℚ)))
  change
    Module.finrank ℚ
        (((numberFieldSeparableClosureEmbedding F).fieldRange ⊓
          rationalCyclotomicZHatField :
          IntermediateField ℚ (SeparableClosure ℚ))) =
      Module.finrank ℚ
        ((LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field ⊓ rationalCyclotomicZHatField :
          IntermediateField ℚ (SeparableClosure ℚ)))
  exact
    abstractFixedFieldCyclotomicZHatIntersection_finrank_eq_of_embedding
      H (numberFieldSeparableClosureEmbedding F)

theorem
    cyclotomicZHatIntersectionDegree_abstractFixedField_eq_residueDegree
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    let F :=
      LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field
    letI : FiniteDimensional ℚ F :=
      LocalClassFieldTheory.abstractFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ) H.field H.finite
    letI : NumberField F :=
      NumberField.of_module_finite ℚ F
    cyclotomicZHatIntersectionDegree F =
      (H.residueDegree rationalCyclotomicDegreeData : ℕ) := by
  exact
    (cyclotomicZHatIntersectionDegree_abstractFixedField_eq_intersection_finrank
      H).trans
      (rationalCyclotomicDegreeData_residueDegree_eq_intersection_finrank
        H).symm

theorem cyclotomicZHatIntersectionDegree_pos :
    0 < cyclotomicZHatIntersectionDegree K

theorem cyclotomicZHatIntersectionDegree_dvd_finrank :
    cyclotomicZHatIntersectionDegree K ∣
      Module.finrank ℚ K

theorem
    rationalCyclotomicZHatFieldGal_fixingSubgroup_image_eq_mulNat_range :
    (((numberFieldCyclotomicZHatIntersection K).restrict
          (show
            numberFieldCyclotomicZHatIntersection K ≤
              rationalCyclotomicZHatField from
            inf_le_right)).fixingSubgroup.map
        rationalCyclotomicZHatFieldGalEquivZHat.toMonoidHom).toAddSubgroup' =
      (zHatMulNat
        (cyclotomicZHatIntersectionDegree K)).toAddMonoidHom.range := by
  let hle :
      numberFieldCyclotomicZHatIntersection K ≤
        rationalCyclotomicZHatField :=
    inf_le_right
  let E : IntermediateField ℚ rationalCyclotomicZHatField :=
    (numberFieldCyclotomicZHatIntersection K).restrict hle
  let e :=
    rationalCyclotomicZHatFieldGalEquivZHat
  change
    (E.fixingSubgroup.map
      e.toMonoidHom).toAddSubgroup' =
        (zHatMulNat
          (cyclotomicZHatIntersectionDegree K)).toAddMonoidHom.range
  refine
    zHatAddSubgroup_eq_mulNat_range_of_index_eq
      (E.fixingSubgroup.map
        e.toMonoidHom).toAddSubgroup'
      (cyclotomicZHatIntersectionDegree_pos K) ?_
  change
    (E.fixingSubgroup.map e.toMonoidHom).index =
      cyclotomicZHatIntersectionDegree K
  calc
    (E.fixingSubgroup.map e.toMonoidHom).index = E.fixingSubgroup.index :=
      Subgroup.index_map_equiv E.fixingSubgroup e.toMulEquiv
    _ = Module.finrank ℚ E :=
      (IntermediateField.finrank_eq_fixingSubgroup_index rationalCyclotomicZHatField E).symm
    _ = cyclotomicZHatIntersectionDegree K := by
      change
        Module.finrank ℚ
            ((numberFieldCyclotomicZHatIntersection K).restrict hle) =
          Module.finrank ℚ (numberFieldCyclotomicZHatIntersection K)
      exact
        ((IntermediateField.restrictAlgEquiv hle).toLinearEquiv).finrank_eq.symm

def numberFieldCyclotomicZHatFiniteCompositum
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    IntermediateField ℚ (SeparableClosure ℚ)

instance
    numberFieldCyclotomicZHatFiniteCompositum_finiteDimensional
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    FiniteDimensional ℚ
      (numberFieldCyclotomicZHatFiniteCompositum K E)

instance
    numberFieldCyclotomicZHatFiniteCompositum_numberField
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    NumberField
      (numberFieldCyclotomicZHatFiniteCompositum K E)

def
    numberFieldCyclotomicZHatFiniteCompositumEmbedding
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    K →ₐ[ℚ] numberFieldCyclotomicZHatFiniteCompositum K E

def
    rationalCyclotomicZHatFiniteLayerCompositumEmbedding
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    E →ₐ[ℚ] numberFieldCyclotomicZHatFiniteCompositum K E

instance
    numberFieldCyclotomicZHatFiniteCompositum_algebra
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    Algebra K
      (numberFieldCyclotomicZHatFiniteCompositum K E)

instance
    rationalCyclotomicZHatFiniteLayerCompositum_algebra
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    Algebra E
      (numberFieldCyclotomicZHatFiniteCompositum K E)

instance
    rationalCyclotomicZHatFiniteLayerCompositum_smul
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    SMul E
      (numberFieldCyclotomicZHatFiniteCompositum K E)

def numberFieldCyclotomicZHatFiniteIntersection
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    IntermediateField ℚ E

theorem
    numberFieldCyclotomicZHatFiniteIntersection_coe_mem_intersection
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField)
    (x : E)
    (hx :
      x ∈ numberFieldCyclotomicZHatFiniteIntersection K E) :
    ((((x : E) : rationalCyclotomicZHatField) :
        SeparableClosure ℚ)) ∈
      numberFieldCyclotomicZHatIntersection K

instance
    numberFieldCyclotomicZHatFiniteCompositum_scalarTower
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    IsScalarTower ℚ K
      (numberFieldCyclotomicZHatFiniteCompositum K E)

instance
    rationalCyclotomicZHatFiniteLayerCompositum_scalarTower
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    IsScalarTower ℚ E
      (numberFieldCyclotomicZHatFiniteCompositum K E)

instance
    numberFieldCyclotomicZHatFiniteCompositum_finiteDimensional_over_K
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    FiniteDimensional K
      (numberFieldCyclotomicZHatFiniteCompositum K E)

instance
    numberFieldCyclotomicZHatFiniteCompositum_finiteDimensional_over_layer
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    FiniteDimensional E
      (numberFieldCyclotomicZHatFiniteCompositum K E)

instance
    numberFieldCyclotomicZHatFiniteCompositum_isGalois
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    IsGalois K
      (numberFieldCyclotomicZHatFiniteCompositum K E)

instance
    numberFieldCyclotomicZHatFiniteCompositum_isAbelianGalois
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    IsAbelianGalois K
      (numberFieldCyclotomicZHatFiniteCompositum K E)

theorem
    numberFieldCyclotomicZHatFiniteCompositum_restriction_range
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    letI : Normal ℚ E := E.isGalois.to_normal
    let C :=
      numberFieldCyclotomicZHatFiniteCompositum K E
    (IntermediateField.restrictRestrictAlgEquivMapHom
        ℚ E K C).range =
      (numberFieldCyclotomicZHatFiniteIntersection K E).fixingSubgroup := by
  let : Normal ℚ E := E.isGalois.to_normal
  let C :=
    numberFieldCyclotomicZHatFiniteCompositum K E
  let : Algebra ℚ C := C.algebra'
  let : Algebra K C :=
    numberFieldCyclotomicZHatFiniteCompositum_algebra K E
  let : IsScalarTower ℚ K C :=
    numberFieldCyclotomicZHatFiniteCompositum_scalarTower K E
  let : Algebra E C :=
    rationalCyclotomicZHatFiniteLayerCompositum_algebra K E
  let : IsScalarTower ℚ E C :=
    rationalCyclotomicZHatFiniteLayerCompositum_scalarTower K E
  let eK : K →ₐ[ℚ] C :=
    numberFieldCyclotomicZHatFiniteCompositumEmbedding K E
  let eE : E →ₐ[ℚ] C :=
    rationalCyclotomicZHatFiniteLayerCompositumEmbedding K E
  let r :
      (C ≃ₐ[K] C) →* (E ≃ₐ[ℚ] E) :=
    IntermediateField.restrictRestrictAlgEquivMapHom
      ℚ E K C
  let J : IntermediateField ℚ E :=
    numberFieldCyclotomicZHatFiniteIntersection K E
  have restriction_commutes
      (τ : C ≃ₐ[K] C) (x : E) :
      eE (r τ x) = τ (eE x) := by
    change algebraMap E C (r τ x) = τ (algebraMap E C x)
    change
      algebraMap E C
          ((AlgEquiv.restrictNormal
            (MulSemiringAction.toAlgEquiv ℚ C τ) E) x) =
        (MulSemiringAction.toAlgEquiv ℚ C τ) (algebraMap E C x)
    exact AlgEquiv.restrictNormal_commutes
      (MulSemiringAction.toAlgEquiv ℚ C τ) E x
  have hfixedField :
      IntermediateField.fixedField r.range = J := by
    ext x
    rw [IntermediateField.mem_fixedField_iff]
    change
      (∀ σ, σ ∈ r.range → σ x = x) ↔
        eE x ∈ eK.fieldRange
    constructor
    · intro hx
      have hfixed :
          ∀ τ : C ≃ₐ[K] C, τ (eE x) = eE x := by
        intro τ
        have hxτ :
            r τ x = x :=
          hx (r τ) ⟨τ, rfl⟩
        have hrestrict :
            eE (r τ x) = τ (eE x) := by
          exact restriction_commutes τ x
        exact hrestrict.symm.trans (congrArg eE hxτ)
      have hmem :
          eE x ∈ Set.range (algebraMap K C) :=
        (IsGalois.mem_range_algebraMap_iff_fixed
          (eE x)).2 hfixed
      rw [AlgHom.mem_fieldRange]
      obtain ⟨k, hk⟩ := hmem
      refine ⟨k, ?_⟩
      change algebraMap K C k = eE x
      exact hk
    · intro hx σ hσ
      obtain ⟨τ, rfl⟩ := hσ
      rw [AlgHom.mem_fieldRange] at hx
      obtain ⟨k, hk⟩ := hx
      apply eE.injective
      change eE (r τ x) = eE x
      have hrestrict :
          eE (r τ x) = τ (eE x) := by
        exact restriction_commutes τ x
      rw [hrestrict, ← hk]
      change τ (algebraMap K C k) = algebraMap K C k
      exact τ.commutes k
  calc
    r.range =
        (IntermediateField.fixedField r.range).fixingSubgroup :=
      (IntermediateField.fixingSubgroup_fixedField
        r.range).symm
    _ = J.fixingSubgroup := by rw [hfixedField]

def numberFieldCyclotomicZHatCompositum :
    IntermediateField ℚ (SeparableClosure ℚ)

def numberFieldCyclotomicZHatCompositumEmbedding :
    K →ₐ[ℚ] numberFieldCyclotomicZHatCompositum K

def rationalCyclotomicZHatCompositumEmbedding :
    rationalCyclotomicZHatField →ₐ[ℚ]
      numberFieldCyclotomicZHatCompositum K

instance numberFieldCyclotomicZHatCompositum_algebra :
    Algebra K (numberFieldCyclotomicZHatCompositum K)

instance rationalCyclotomicZHatCompositum_algebra :
    Algebra rationalCyclotomicZHatField
      (numberFieldCyclotomicZHatCompositum K)

instance numberFieldCyclotomicZHatCompositum_scalarTower :
    IsScalarTower ℚ K
      (numberFieldCyclotomicZHatCompositum K)

instance rationalCyclotomicZHatCompositum_scalarTower :
    IsScalarTower ℚ rationalCyclotomicZHatField
      (numberFieldCyclotomicZHatCompositum K)

instance
    numberFieldCyclotomicZHatCompositum_isGalois :
    IsGalois K (numberFieldCyclotomicZHatCompositum K)

instance
    numberFieldCyclotomicZHatCompositum_isAbelianGalois :
    IsAbelianGalois K
      (numberFieldCyclotomicZHatCompositum K)

def
    numberFieldCyclotomicZHatFiniteCompositumInclusion
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    numberFieldCyclotomicZHatFiniteCompositum K E →ₐ[ℚ]
      numberFieldCyclotomicZHatCompositum K

def
    numberFieldCyclotomicZHatFiniteCompositumInclusionOverBase
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    numberFieldCyclotomicZHatFiniteCompositum K E →ₐ[K]
      numberFieldCyclotomicZHatCompositum K

def
    numberFieldCyclotomicZHatFiniteLayerInCompositum
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    IntermediateField K
      (numberFieldCyclotomicZHatCompositum K)

instance
    numberFieldCyclotomicZHatFiniteLayerInCompositum_finiteDimensional
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    FiniteDimensional K
      (numberFieldCyclotomicZHatFiniteLayerInCompositum K E)

instance
    numberFieldCyclotomicZHatFiniteLayerInCompositum_isAbelianGalois
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    IsAbelianGalois K
      (numberFieldCyclotomicZHatFiniteLayerInCompositum K E)

instance
    numberFieldCyclotomicZHatFiniteLayerInCompositum_numberField
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    NumberField
      (numberFieldCyclotomicZHatFiniteLayerInCompositum K E)

instance
    numberFieldCyclotomicZHatFiniteLayerInCompositum_scalarTower
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    IsScalarTower ℚ K
      (numberFieldCyclotomicZHatFiniteLayerInCompositum K E)

def
    rationalCyclotomicZHatFiniteLayerInCompositumEmbedding
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    E →ₐ[ℚ]
      numberFieldCyclotomicZHatFiniteLayerInCompositum K E

instance
    rationalCyclotomicZHatFiniteLayerInCompositum_algebra
  (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    Algebra E
      (numberFieldCyclotomicZHatFiniteLayerInCompositum K E)

instance
    rationalCyclotomicZHatFiniteLayerInCompositum_smul
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    SMul E
      (numberFieldCyclotomicZHatFiniteLayerInCompositum K E)

instance
    rationalCyclotomicZHatFiniteLayerInCompositum_scalarTower
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    IsScalarTower ℚ E
      (numberFieldCyclotomicZHatFiniteLayerInCompositum K E)

def
    numberFieldCyclotomicZHatFiniteGaloisLayerInCompositum
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    FiniteGaloisIntermediateField K
      (numberFieldCyclotomicZHatCompositum K) where
  toIntermediateField :=
    numberFieldCyclotomicZHatFiniteLayerInCompositum K E
  finiteDimensional := inferInstance
  isGalois := inferInstance

def numberFieldCyclotomicZHatCompositumRestriction :
    Gal((numberFieldCyclotomicZHatCompositum K)/K) →*
      Gal(rationalCyclotomicZHatField/ℚ)

theorem numberFieldCyclotomicZHatCompositumRestriction_injective :
    Function.Injective
      (numberFieldCyclotomicZHatCompositumRestriction K)

theorem
    restrictNormalHom_numberFieldCyclotomicZHatCompositumRestriction
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField)
    (σ :
      Gal((numberFieldCyclotomicZHatCompositum K)/K)) :
    letI : Algebra ℚ (numberFieldCyclotomicZHatCompositum K) :=
      (numberFieldCyclotomicZHatCompositum K).algebra'
    letI : Algebra K (numberFieldCyclotomicZHatCompositum K) :=
      numberFieldCyclotomicZHatCompositum_algebra K
    letI : IsScalarTower ℚ K (numberFieldCyclotomicZHatCompositum K) :=
      numberFieldCyclotomicZHatCompositum_scalarTower K
    letI : Normal ℚ E := E.isGalois.to_normal
    letI : Normal K
        (numberFieldCyclotomicZHatFiniteLayerInCompositum K E) := by
      let : IsAbelianGalois K
          (numberFieldCyclotomicZHatFiniteLayerInCompositum K E) :=
        numberFieldCyclotomicZHatFiniteLayerInCompositum_isAbelianGalois K E
      exact IsGalois.to_normal
    letI : IsScalarTower K
        (numberFieldCyclotomicZHatFiniteLayerInCompositum K E)
        (numberFieldCyclotomicZHatCompositum K) := by
      exact IntermediateField.isScalarTower_mid
        (numberFieldCyclotomicZHatFiniteLayerInCompositum K E)
    AlgEquiv.restrictNormalHom E
        (numberFieldCyclotomicZHatCompositumRestriction K σ) =
      IntermediateField.restrictRestrictAlgEquivMapHom
          ℚ E K
        (numberFieldCyclotomicZHatFiniteLayerInCompositum K E)
        (AlgEquiv.restrictNormalHom
          (numberFieldCyclotomicZHatFiniteLayerInCompositum K E)
          σ) := by
  let : Normal ℚ E := E.isGalois.to_normal
  let : Algebra ℚ (numberFieldCyclotomicZHatCompositum K) :=
    (numberFieldCyclotomicZHatCompositum K).algebra'
  let : Algebra K (numberFieldCyclotomicZHatCompositum K) :=
    numberFieldCyclotomicZHatCompositum_algebra K
  let : IsScalarTower ℚ K (numberFieldCyclotomicZHatCompositum K) :=
    numberFieldCyclotomicZHatCompositum_scalarTower K
  let : Normal K
      (numberFieldCyclotomicZHatFiniteLayerInCompositum K E) := by
    let : IsAbelianGalois K
        (numberFieldCyclotomicZHatFiniteLayerInCompositum K E) :=
      numberFieldCyclotomicZHatFiniteLayerInCompositum_isAbelianGalois K E
    exact IsGalois.to_normal
  let : IsScalarTower K
      (numberFieldCyclotomicZHatFiniteLayerInCompositum K E)
      (numberFieldCyclotomicZHatCompositum K) := by
    exact IntermediateField.isScalarTower_mid
      (numberFieldCyclotomicZHatFiniteLayerInCompositum K E)
  let C := numberFieldCyclotomicZHatCompositum K
  let T := rationalCyclotomicZHatField
  let P : IntermediateField K C :=
    numberFieldCyclotomicZHatFiniteLayerInCompositum K E
  let : Algebra T C := rationalCyclotomicZHatCompositum_algebra K
  let : IsScalarTower ℚ T C :=
    rationalCyclotomicZHatCompositum_scalarTower K
  let : Algebra E P :=
    rationalCyclotomicZHatFiniteLayerInCompositum_algebra K E
  let : IsScalarTower ℚ E P :=
    rationalCyclotomicZHatFiniteLayerInCompositum_scalarTower K E
  let : IsAbelianGalois K P := by
    change IsAbelianGalois K
      (numberFieldCyclotomicZHatFiniteLayerInCompositum K E)
    exact numberFieldCyclotomicZHatFiniteLayerInCompositum_isAbelianGalois K E
  let : Normal K P := IsGalois.to_normal
  let eEP : E →ₐ[ℚ] P :=
    rationalCyclotomicZHatFiniteLayerInCompositumEmbedding K E
  let iP : P →ₐ[K] C := IntermediateField.val P
  let iT : T →ₐ[ℚ] C := rationalCyclotomicZHatCompositumEmbedding K
  have hEmbedding (z : E) :
      iP (eEP z) = iT (z : T) := by
    apply Subtype.ext
    rfl
  have hL (z : E) :
      ((AlgEquiv.restrictNormalHom E
        (numberFieldCyclotomicZHatCompositumRestriction K σ)) z : T) =
        (numberFieldCyclotomicZHatCompositumRestriction K σ) (z : T) := by
    change
      algebraMap E T
          ((AlgEquiv.restrictNormalHom E
            (numberFieldCyclotomicZHatCompositumRestriction K σ)) z) =
        (numberFieldCyclotomicZHatCompositumRestriction K σ)
          (algebraMap E T z)
    change
      algebraMap E T
          ((AlgEquiv.restrictNormal
            (numberFieldCyclotomicZHatCompositumRestriction K σ) E) z) =
        (numberFieldCyclotomicZHatCompositumRestriction K σ)
          (algebraMap E T z)
    exact AlgEquiv.restrictNormal_commutes
      (numberFieldCyclotomicZHatCompositumRestriction K σ) E z
  have hRaw (z : T) :
      iT (numberFieldCyclotomicZHatCompositumRestriction K σ z) =
        σ (iT z) := by
    change
      algebraMap T C
          (numberFieldCyclotomicZHatCompositumRestriction K σ z) =
        σ (algebraMap T C z)
    change
      algebraMap T C
          ((AlgEquiv.restrictNormal
            (MulSemiringAction.toAlgEquiv ℚ C σ) T) z) =
        (MulSemiringAction.toAlgEquiv ℚ C σ) (algebraMap T C z)
    exact AlgEquiv.restrictNormal_commutes
      (MulSemiringAction.toAlgEquiv ℚ C σ) T z
  have hP (z : P) :
      iP (AlgEquiv.restrictNormalHom P σ z) = σ (iP z) := by
    change
      algebraMap P C (AlgEquiv.restrictNormalHom P σ z) =
        σ (algebraMap P C z)
    change
      algebraMap P C
          ((AlgEquiv.restrictNormal
            (MulSemiringAction.toAlgEquiv K C σ) P) z) =
        (MulSemiringAction.toAlgEquiv K C σ) (algebraMap P C z)
    exact AlgEquiv.restrictNormal_commutes
      (MulSemiringAction.toAlgEquiv K C σ) P z
  have hQ (z : E) :
      eEP
          (IntermediateField.restrictRestrictAlgEquivMapHom
            ℚ E K P (AlgEquiv.restrictNormalHom P σ) z) =
        (AlgEquiv.restrictNormalHom P σ) (eEP z) := by
    change
      algebraMap E P
          (IntermediateField.restrictRestrictAlgEquivMapHom
            ℚ E K P (AlgEquiv.restrictNormalHom P σ) z) =
        (AlgEquiv.restrictNormalHom P σ) (algebraMap E P z)
    change
      algebraMap E P
          ((AlgEquiv.restrictNormal
            (MulSemiringAction.toAlgEquiv ℚ P
              (AlgEquiv.restrictNormalHom P σ)) E) z) =
        (MulSemiringAction.toAlgEquiv ℚ P
          (AlgEquiv.restrictNormalHom P σ)) (algebraMap E P z)
    exact AlgEquiv.restrictNormal_commutes
      (MulSemiringAction.toAlgEquiv ℚ P
        (AlgEquiv.restrictNormalHom P σ)) E z
  apply AlgEquiv.ext
  intro x
  apply eEP.injective
  apply iP.injective
  calc
    iP (eEP
        (AlgEquiv.restrictNormalHom E
          (numberFieldCyclotomicZHatCompositumRestriction K σ) x)) =
        iT (((AlgEquiv.restrictNormalHom E
          (numberFieldCyclotomicZHatCompositumRestriction K σ) x) : T)) :=
      hEmbedding _
    _ = iT
        (numberFieldCyclotomicZHatCompositumRestriction K σ (x : T)) :=
      congrArg iT (hL x)
    _ = σ (iT (x : T)) := hRaw (x : T)
    _ = σ (iP (eEP x)) := congrArg σ (hEmbedding x).symm
    _ = iP (AlgEquiv.restrictNormalHom P σ (eEP x)) := (hP (eEP x)).symm
    _ = iP (eEP
        (IntermediateField.restrictRestrictAlgEquivMapHom
          ℚ E K P (AlgEquiv.restrictNormalHom P σ) x)) :=
      congrArg iP (hQ x).symm

theorem numberFieldCyclotomicZHatCompositumRestriction_continuous :
    Continuous
      (numberFieldCyclotomicZHatCompositumRestriction K)