CyclotomicIdeleValue.lean

def rationalCyclotomicZHatIdeleValue :
    IdeleGroup ℚ →ₜ* Multiplicative ZHat

theorem rationalCyclotomicZHatIdeleValue_apply
    (a : IdeleGroup ℚ) :
    rationalCyclotomicZHatIdeleValue a =
      rationalCyclotomicZHatFieldGalEquivZHat
        (rationalCyclotomicZHatGlobalArtin a)

theorem rationalCyclotomicZHatIdeleValue_denseRange :
    DenseRange rationalCyclotomicZHatIdeleValue

theorem rationalCyclotomicZHatIdeleValue_normOne_denseRange :
    DenseRange
      (fun b : IdeleGroup.normOneSubgroup (K := ℚ) =>
        rationalCyclotomicZHatIdeleValue b) := by
  change
    DenseRange
      (fun b : IdeleGroup.normOneSubgroup (K := ℚ) =>
        rationalCyclotomicZHatFieldGalEquivZHat
          (rationalCyclotomicZHatGlobalArtin b))
  exact
    rationalCyclotomicZHatFieldGalEquivZHat.surjective.denseRange.comp
      rationalCyclotomicZHatGlobalArtin_normOne_denseRange
      rationalCyclotomicZHatFieldGalEquivZHat.continuous

instance
    (E : FiniteGaloisIntermediateField
      ℚ rationalCyclotomicZHatField) :
    IsAbelianGalois ℚ E

theorem
    numberFieldCyclotomicZHatCompositumRestriction_infiniteGlobalArtinMonoidHom
    (a : IdeleGroup K) :
    numberFieldCyclotomicZHatCompositumRestriction K
        (infiniteGlobalArtinMonoidHom K
          (numberFieldCyclotomicZHatCompositum K) a) =
      rationalCyclotomicZHatGlobalArtin
        (IdeleGroup.norm ℚ K a)

theorem cyclotomicZHatIntersectionDegree_rat :
    cyclotomicZHatIntersectionDegree ℚ = 1

def cyclotomicZHatNormComposite :
    Additive (IdeleGroup K) →+ ZHat

theorem cyclotomicZHatNormComposite_apply
    (a : IdeleGroup K) :
    cyclotomicZHatNormComposite K (Additive.ofMul a) =
      Multiplicative.toAdd
        (rationalCyclotomicZHatIdeleValue
          (IdeleGroup.norm ℚ K a))

theorem cyclotomicZHatNormComposite_baseIdeleInclusion
    (a : IdeleGroup ℚ) :
    cyclotomicZHatNormComposite K
        (Additive.ofMul
          (relativeIdeleBaseChangeMulEquiv
            (K := ℚ) (L := K)
            (RelativeIdeleGroup.inclusion ℚ K a))) =
      Module.finrank ℚ K •
        Multiplicative.toAdd
          (rationalCyclotomicZHatIdeleValue a)

theorem
    nsmulImage_rationalCyclotomicZHatIdeleValue_range_le_normComposite_range :
    nsmulImage
        ((AddEquiv.additiveMultiplicative ZHat).toAddMonoidHom.comp
          (MonoidHom.toAdditive
            rationalCyclotomicZHatIdeleValue.toMonoidHom)).range
        (Module.finrank ℚ K) ≤
      (cyclotomicZHatNormComposite K).range

theorem finiteCyclotomicLayer_normArtin_range
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    letI : NumberField E :=
      NumberField.of_module_finite ℚ E
    let C :=
      numberFieldCyclotomicZHatFiniteCompositum K E
    ((globalArtinMonoidHom
        (K := ℚ) (L := E)).comp
          (IdeleGroup.norm ℚ K)).range =
      (IntermediateField.restrictRestrictAlgEquivMapHom
        ℚ E K C).range := by
  let : NumberField E :=
    NumberField.of_module_finite ℚ E
  let C :=
    numberFieldCyclotomicZHatFiniteCompositum K E
  let r :
      (C ≃ₐ[K] C) →* (E ≃ₐ[ℚ] E) :=
    IntermediateField.restrictRestrictAlgEquivMapHom
      ℚ E K C
  have hcomm :
      r.comp
          (globalArtinMonoidHom
            (K := K) (L := C)) =
        (globalArtinMonoidHom
          (K := ℚ) (L := E)).comp
            (IdeleGroup.norm ℚ K) :=
    by
      have hr :
          r =
            (AlgEquiv.restrictNormalHom E).comp
              (AlgEquiv.restrictScalarsHom ℚ) := by
        ext σ x
        exact rfl
      rw [hr]
      exact
        globalArtinMonoidHom_norm_restriction
          (K := ℚ) (L := E) (K' := K) (L' := C)
  apply le_antisymm
  · rintro σ ⟨a, rfl⟩
    refine
      ⟨globalArtinMonoidHom
          (K := K) (L := C) a,
        ?_⟩
    exact DFunLike.congr_fun hcomm a
  · rintro σ ⟨τ, rfl⟩
    obtain ⟨a, ha⟩ :=
      globalArtinMonoidHom_surjective
        (K := K) (L := C) τ
    refine ⟨a, ?_⟩
    have h := DFunLike.congr_fun hcomm a
    change
      r (globalArtinMonoidHom (K := K) (L := C) a) =
        globalArtinMonoidHom
          (K := ℚ) (L := E) (IdeleGroup.norm ℚ K a) at h
    calc
      globalArtinMonoidHom
            (K := ℚ) (L := E) (IdeleGroup.norm ℚ K a) =
          r (globalArtinMonoidHom (K := K) (L := C) a) := h.symm
      _ = r τ := congrArg r ha

theorem finiteCyclotomicLayer_normArtin_range_eq_fixingSubgroup
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    letI : NumberField E :=
      NumberField.of_module_finite ℚ E
    ((globalArtinMonoidHom
        (K := ℚ) (L := E)).comp
          (IdeleGroup.norm ℚ K)).range =
      (numberFieldCyclotomicZHatFiniteIntersection K E).fixingSubgroup := by
  let : NumberField E :=
    NumberField.of_module_finite ℚ E
  rw [finiteCyclotomicLayer_normArtin_range K E]
  exact
    numberFieldCyclotomicZHatFiniteCompositum_restriction_range
      K E

theorem
    ideleNorm_mem_cyclotomicZHatIntersection_relativeIdeleNorm_range
    (a : IdeleGroup K) :
    let hle :
        numberFieldCyclotomicZHatIntersection K ≤
          rationalCyclotomicZHatField :=
      inf_le_right
    let E :=
      (numberFieldCyclotomicZHatIntersection K).restrict hle
    letI : FiniteDimensional ℚ E :=
      (IntermediateField.restrictAlgEquiv hle).toLinearEquiv.finiteDimensional
    letI : NumberField E :=
      NumberField.of_module_finite ℚ E
    IdeleGroup.norm ℚ K a ∈
      (RelativeIdeleGroup.norm ℚ E).range := by
  let hle :
      numberFieldCyclotomicZHatIntersection K ≤
        rationalCyclotomicZHatField :=
    inf_le_right
  let E :=
    (numberFieldCyclotomicZHatIntersection K).restrict hle
  let : FiniteDimensional ℚ E :=
    (IntermediateField.restrictAlgEquiv hle).toLinearEquiv.finiteDimensional
  let : NumberField E :=
    NumberField.of_module_finite ℚ E
  let eEK : E →ₐ[ℚ] K :=
    (numberFieldCyclotomicZHatIntersectionEmbedding K).comp
      (IntermediateField.restrictAlgEquiv hle).symm.toAlgHom
  let : Algebra E K :=
    eEK.toRingHom.toAlgebra
  let : IsScalarTower ℚ E K :=
    IsScalarTower.of_algebraMap_eq'
      eEK.comp_algebraMap.symm
  let : FiniteDimensional E K :=
    FiniteDimensional.right ℚ E K
  let b : RelativeIdeleGroup ℚ K :=
    (relativeIdeleBaseChangeMulEquiv
      (K := ℚ) (L := K)).symm a
  let t : TowerRelativeIdeleGroup ℚ E K :=
    (towerRelativeIdeleEquiv ℚ E K).symm b
  refine
    ⟨TowerRelativeIdeleGroup.norm ℚ E K t,
      ?_⟩
  calc
    RelativeIdeleGroup.norm ℚ E
          (TowerRelativeIdeleGroup.norm
            ℚ E K t) =
        RelativeIdeleGroup.norm ℚ K
          (towerRelativeIdeleEquiv
            ℚ E K t) :=
      TowerRelativeIdeleGroup.norm_transitive_flatten ℚ E K t
    _ = RelativeIdeleGroup.norm ℚ K b := by
      rw [show
        towerRelativeIdeleEquiv ℚ E K t = b by
          simp [t]]
    _ = IdeleGroup.norm ℚ K
          (relativeIdeleBaseChangeMulEquiv
            (K := ℚ) (L := K) b) :=
      (IdeleGroup.norm_relativeIdeleBaseChangeMulEquiv
        ℚ K b).symm
    _ = IdeleGroup.norm ℚ K a := by
      rw [show
        relativeIdeleBaseChangeMulEquiv
            (K := ℚ) (L := K) b = a by
          simp [b]]

theorem
    rationalCyclotomicZHatGlobalArtin_norm_mem_intersection_fixingSubgroup
    (a : IdeleGroup K) :
    rationalCyclotomicZHatGlobalArtin
          (IdeleGroup.norm ℚ K a) ∈
      ((numberFieldCyclotomicZHatIntersection K).restrict
        (show
          numberFieldCyclotomicZHatIntersection K ≤
            rationalCyclotomicZHatField from
          inf_le_right)).fixingSubgroup := by
  let hle :
      numberFieldCyclotomicZHatIntersection K ≤
        rationalCyclotomicZHatField :=
    inf_le_right
  let E₀ :=
    (numberFieldCyclotomicZHatIntersection K).restrict hle
  let : FiniteDimensional ℚ E₀ :=
    (IntermediateField.restrictAlgEquiv hle).toLinearEquiv.finiteDimensional
  let : NumberField E₀ :=
    NumberField.of_module_finite ℚ E₀
  let : IsAbelianGalois ℚ rationalCyclotomicZHatField :=
    rationalCyclotomicZHatField_isAbelianGalois
  let inclusion : E₀ →ₐ[ℚ] rationalCyclotomicZHatField :=
    E₀.val.toRingHom.toRatAlgHom
  let E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField :=
    { toIntermediateField := E₀
      finiteDimensional := inferInstance
      isGalois :=
        (IsAbelianGalois.of_algHom (K := ℚ) (L := E₀)
          (M := rationalCyclotomicZHatField) inclusion).toIsGalois }
  let : NumberField E :=
    NumberField.of_module_finite ℚ E
  have hnorm :
      IdeleGroup.norm ℚ K a ∈
        (RelativeIdeleGroup.norm ℚ E).range := by
    change
      IdeleGroup.norm ℚ K a ∈
        (RelativeIdeleGroup.norm ℚ E₀).range
    simpa only [E₀, hle] using
      ideleNorm_mem_cyclotomicZHatIntersection_relativeIdeleNorm_range
        K a
  obtain ⟨z, hz⟩ := hnorm
  let : IsAbelianGalois ℚ E :=
    IsAbelianGalois.of_algHom (K := ℚ) (L := E)
      (M := rationalCyclotomicZHatField)
      (show E →ₐ[ℚ] rationalCyclotomicZHatField from
        E.toIntermediateField.val.toRingHom.toRatAlgHom)
  have hfinite :
      globalArtinMonoidHom
          (K := ℚ) (L := E)
          (IdeleGroup.norm ℚ K a) =
        1 := by
    rw [← hz]
    exact
      globalArtinMonoidHom_relativeIdeleNorm_eq_one
        (K := ℚ) (L := E) z
  change
    rationalCyclotomicZHatGlobalArtin
          (IdeleGroup.norm ℚ K a) ∈
      E.fixingSubgroup
  rw [
    FiniteGaloisIntermediateField.mem_fixingSubgroup_iff]
  calc
    AlgEquiv.restrictNormalHom E
          (rationalCyclotomicZHatGlobalArtin
            (IdeleGroup.norm ℚ K a)) =
        globalArtinMonoidHom
          (K := ℚ) (L := E) (IdeleGroup.norm ℚ K a) :=
      restrictNormalHom_rationalCyclotomicZHatGlobalArtin
        (IdeleGroup.norm ℚ K a) E
    _ = 1 := hfinite

theorem
    rationalCyclotomicZHatGlobalArtin_norm_denseRange_in_intersection_fixingSubgroup :
    let hle :
        numberFieldCyclotomicZHatIntersection K ≤
          rationalCyclotomicZHatField :=
      inf_le_right
    let F :=
      (numberFieldCyclotomicZHatIntersection K).restrict hle
    DenseRange
      (fun a : IdeleGroup K =>
        (⟨rationalCyclotomicZHatGlobalArtin
              (IdeleGroup.norm ℚ K a),
            rationalCyclotomicZHatGlobalArtin_norm_mem_intersection_fixingSubgroup
              K a⟩ :
          F.fixingSubgroup)) := by
  let hle :
      numberFieldCyclotomicZHatIntersection K ≤
        rationalCyclotomicZHatField :=
    inf_le_right
  let F :=
    (numberFieldCyclotomicZHatIntersection K).restrict hle
  change
    DenseRange
      (fun a : IdeleGroup K =>
        (⟨rationalCyclotomicZHatGlobalArtin
              (IdeleGroup.norm ℚ K a),
            rationalCyclotomicZHatGlobalArtin_norm_mem_intersection_fixingSubgroup
              K a⟩ :
          F.fixingSubgroup))
  apply dense_iff_inter_open.mpr
  rintro U hU ⟨σ, hσU⟩
  rw [isOpen_induced_iff] at hU
  obtain ⟨U₀, hU₀open, hUeq⟩ := hU
  have hσU₀ :
      σ.1 ∈ U₀ := by
    have hσpre :
        σ ∈
          Subtype.val ⁻¹' U₀ := by
      exact hUeq.symm ▸ hσU
    exact hσpre
  let V :
      Set
        (rationalCyclotomicZHatField ≃ₐ[ℚ]
          rationalCyclotomicZHatField) :=
    (Homeomorph.mulLeft
      σ.1) ⁻¹' U₀
  have hVopen : IsOpen V :=
    hU₀open.preimage
      (Homeomorph.mulLeft
        σ.1).continuous
  have hVone : ((1 : F.fixingSubgroup).1) ∈ V := by
    change
      σ.1 * (1 : F.fixingSubgroup).1 ∈ U₀
    rw [show
      σ.1 * (1 : F.fixingSubgroup).1 = σ.1 by
        exact congrArg Subtype.val (mul_one σ)]
    exact hσU₀
  have hVnhds :
      V ∈ 𝓝 ((1 : F.fixingSubgroup).1) :=
    hVopen.mem_nhds hVone
  have hkrull :=
    InfiniteGalois.krullTopology_mem_nhds_one_iff_of_isGalois
      (k := ℚ) (K := rationalCyclotomicZHatField) V
  obtain ⟨E, hEV⟩ :=
    hkrull.mp hVnhds
  let hENumberField : NumberField E :=
    NumberField.of_module_finite ℚ E
  let : NumberField E := hENumberField
  let hEAbelian : IsAbelianGalois ℚ E :=
    IsAbelianGalois.of_algHom E.toIntermediateField.val
  let : IsAbelianGalois ℚ E := hEAbelian
  have hσfix :
      ∀ x : rationalCyclotomicZHatField,
        x ∈ F →
          σ.1 x = x := by
    exact
      (IntermediateField.mem_fixingSubgroup_iff F σ.1).1
        σ.property
  have hrestrictFix :
      AlgEquiv.restrictNormalHom E
          σ.1 ∈
        (numberFieldCyclotomicZHatFiniteIntersection K E).fixingSubgroup := by
    rw [IntermediateField.mem_fixingSubgroup_iff]
    intro x hx
    apply Subtype.ext
    have hxF :
        ((x : E) : rationalCyclotomicZHatField) ∈ F := by
      apply
        (IntermediateField.mem_restrict hle
          ((x : E) : rationalCyclotomicZHatField)).2
      exact
        numberFieldCyclotomicZHatFiniteIntersection_coe_mem_intersection
          K E x hx
    calc
      (((AlgEquiv.restrictNormalHom E
            σ.1) x : E) :
          rationalCyclotomicZHatField) =
          σ.1
            ((x : E) : rationalCyclotomicZHatField) :=
        AlgEquiv.restrictNormal_commutes
          σ.1 E x
      _ = ((x : E) : rationalCyclotomicZHatField) :=
        hσfix ((x : E) : rationalCyclotomicZHatField) hxF
  have hrestrictRange :
      AlgEquiv.restrictNormalHom E
          σ.1 ∈
        ((globalArtinMonoidHom
            (K := ℚ) (L := E)).comp
          (IdeleGroup.norm ℚ K)).range := by
    rw [
      finiteCyclotomicLayer_normArtin_range_eq_fixingSubgroup
        K E]
    exact hrestrictFix
  obtain ⟨a, ha⟩ := hrestrictRange
  let τ :
      F.fixingSubgroup :=
    ⟨rationalCyclotomicZHatGlobalArtin
        (IdeleGroup.norm ℚ K a),
      rationalCyclotomicZHatGlobalArtin_norm_mem_intersection_fixingSubgroup
        K a⟩
  let δ : F.fixingSubgroup := σ⁻¹ * τ
  have hδ :
      δ.1 = (σ.1)⁻¹ * τ.1 :=
    rfl
  have hτ :
      τ.1 =
        rationalCyclotomicZHatGlobalArtin
          (IdeleGroup.norm ℚ K a) :=
    rfl
  have ha' :
      globalArtinMonoidHom
          (K := ℚ) (L := E) (IdeleGroup.norm ℚ K a) =
        AlgEquiv.restrictNormalHom E σ.1 := by
    simpa only [MonoidHom.comp_apply] using ha
  have hτProjection :
      AlgEquiv.restrictNormalHom E τ.1 =
        globalArtinMonoidHom
          (K := ℚ) (L := E) (IdeleGroup.norm ℚ K a) := by
    rw [hτ]
    change
      AlgEquiv.restrictNormalHom E
          (infiniteGlobalArtinMonoidHom
            ℚ rationalCyclotomicZHatField
            (IdeleGroup.norm ℚ K a)) =
        globalArtinMonoidHom
          (K := ℚ) (L := E) (IdeleGroup.norm ℚ K a)
    exact
      restrictNormalHom_rationalCyclotomicZHatGlobalArtin_of_structures
        (IdeleGroup.norm ℚ K a) E hENumberField hEAbelian
  have hrestrictEq :
      AlgEquiv.restrictNormalHom E τ.1 =
        AlgEquiv.restrictNormalHom E σ.1 :=
    hτProjection.trans ha'
  have hfixE :
      δ.1 ∈ E.fixingSubgroup := by
    apply
      (IntermediateField.mem_fixingSubgroup_iff
        E.toIntermediateField δ.1).2
    intro x hx
    have hrestrictedValue :=
      congrArg
        (fun f : E ≃ₐ[ℚ] E => f ⟨x, hx⟩)
        hrestrictEq
    have hτx : τ.1 x = σ.1 x := by
      calc
        τ.1 x =
            ((AlgEquiv.restrictNormalHom E τ.1)
              ⟨x, hx⟩ : E) :=
          (AlgEquiv.restrictNormal_commutes
            τ.1 E ⟨x, hx⟩).symm
        _ =
            ((AlgEquiv.restrictNormalHom E σ.1)
              ⟨x, hx⟩ : E) :=
          congrArg Subtype.val hrestrictedValue
        _ = σ.1 x :=
          AlgEquiv.restrictNormal_commutes
            σ.1 E ⟨x, hx⟩
    calc
      δ.1 x = ((σ.1)⁻¹ * τ.1) x :=
        congrArg (fun f => f x) hδ
      _ = (σ.1)⁻¹ (τ.1 x) := rfl
      _ = (σ.1)⁻¹ (σ.1 x) :=
        congrArg
          (fun y : rationalCyclotomicZHatField =>
            (σ.1)⁻¹ y)
          hτx
      _ = x := (σ.1).symm_apply_apply x
  have hmemV :
      δ.1 ∈ V :=
    hEV hfixE
  have hτU₀ :
      τ.1 ∈ U₀ := by
    change σ.1 * δ.1 ∈ U₀ at hmemV
    have hcancel : σ * δ = τ := by
      dsimp only [δ]
      exact mul_inv_cancel_left σ τ
    have hcancelVal := congrArg Subtype.val hcancel
    change σ.1 * δ.1 = τ.1 at hcancelVal
    rw [hcancelVal] at hmemV
    exact hmemV
  have hτU : τ ∈ U := by
    have hτpre : τ ∈ Subtype.val ⁻¹' U₀ :=
      hτU₀
    exact hUeq ▸ hτpre
  exact ⟨τ, hτU, ⟨a, rfl⟩⟩

theorem cyclotomicZHatNormComposite_mem_mulNat_range
    (a : Additive (IdeleGroup K)) :
    cyclotomicZHatNormComposite K a ∈
      (zHatMulNat
        (cyclotomicZHatIntersectionDegree K)).toAddMonoidHom.range

theorem cyclotomicZHatNormComposite_range_le_mulNat_range :
    (cyclotomicZHatNormComposite K).range ≤
      (zHatMulNat
        (cyclotomicZHatIntersectionDegree K)).toAddMonoidHom.range

def cyclotomicZHatNormCompositeInMulNatRange :
    Additive (IdeleGroup K) →+
      (zHatMulNat
        (cyclotomicZHatIntersectionDegree K)).toAddMonoidHom.range

theorem cyclotomicZHatNormCompositeInMulNatRange_denseRange :
    DenseRange
      (cyclotomicZHatNormCompositeInMulNatRange K)

def normalizedCyclotomicZHatIdeleValue :
    Additive (IdeleGroup K) →+ ZHat

theorem normalizedCyclotomicZHatIdeleValue_denseRange :
    DenseRange (normalizedCyclotomicZHatIdeleValue K)

theorem cyclotomicZHatIntersectionDegree_nsmul_normalizedIdeleValue
    (a : Additive (IdeleGroup K)) :
    cyclotomicZHatIntersectionDegree K •
        normalizedCyclotomicZHatIdeleValue K a =
      cyclotomicZHatNormComposite K a

theorem normalizedCyclotomicZHatIdeleValue_baseIdeleInclusion
    (a : IdeleGroup ℚ) :
    normalizedCyclotomicZHatIdeleValue K
        (Additive.ofMul
          (relativeIdeleBaseChangeMulEquiv
            (K := ℚ) (L := K)
            (RelativeIdeleGroup.inclusion ℚ K a))) =
      (Module.finrank ℚ K /
          cyclotomicZHatIntersectionDegree K) •
        Multiplicative.toAdd
          (rationalCyclotomicZHatIdeleValue a)