GlobalNormResidueAbelianizationNaturality.lean

theorem abelianizationNaturalityIdeleClassIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)

theorem rationalIdeleClassEquivFixed_congr_apply_val
    {A B : IntermediateField ℚ (SeparableClosure ℚ)}
    [FiniteDimensional ℚ A] [FiniteDimensional ℚ B]
    (h : A = B)
    (e : B ≃ₐ[ℚ] A)
    (he : e.trans (IntermediateField.equivOfEq h) =
      (AlgEquiv.refl : B ≃ₐ[ℚ] B))
    (c : Additive (IdeleClassGroup B)) :
    ((rationalIdeleClassEquivFixed A)
        (MulEquiv.toAdditive (ideleClassCongr e) c)).1 =
      ((rationalIdeleClassEquivFixed B) c).1

theorem rationalIdeleClassEquivFixed_transport_commonTop_val
    {T : Type} [Field T] [NumberField T]
    {A B : IntermediateField ℚ (SeparableClosure ℚ)}
    [hA : FiniteDimensional ℚ A] [hB : FiniteDimensional ℚ B]
    (h : A = B) (e : T ≃ₐ[ℚ] B) (c : IdeleClassGroup T) :
    ((rationalIdeleClassEquivFixed A)
        (Additive.ofMul (ideleClassCongr (K := T) (M := A)
          (e.trans (IntermediateField.equivOfEq h).symm) c))).1 =
      ((rationalIdeleClassEquivFixed B)
        (Additive.ofMul (ideleClassCongr (K := T) (M := B) e c))).1

theorem
    commonTopBaseIntermediateFiniteDimensional
    [FiniteDimensional K N] : FiniteDimensional K M

theorem
    commonTopIntermediateTopFiniteDimensional
    [FiniteDimensional K N] : FiniteDimensional M N

theorem
    commonTopIntermediateTopIsGalois
    [FiniteDimensional K N] [IsGalois K N] : IsGalois M N

theorem numberFieldEmbeddedBaseSubgroup_le_of_commonTop
    (j : N →ₐ[ℚ] SeparableClosure ℚ) :
    (numberFieldEmbeddedBaseSubgroup M N j).toSubgroup ≤
      (numberFieldEmbeddedBaseSubgroup K N j).toSubgroup

theorem
    numberFieldEmbeddedBaseChangeExtensionQuotient_finite_of_commonTop
    [FiniteDimensional K N] [IsGalois K N]
    (j : N →ₐ[ℚ] SeparableClosure ℚ) :
    let H := numberFieldEmbeddedBaseSubgroup K N j
    let H' := numberFieldEmbeddedBaseSubgroup M N j
    let hH'H := numberFieldEmbeddedBaseSubgroup_le_of_commonTop K M N j
    Finite
      (H.toSubgroup ⧸
        extensionSubgroup H H' hH'H) := by
  dsimp only
  let H := numberFieldEmbeddedBaseSubgroup K N j
  let H' := numberFieldEmbeddedBaseSubgroup M N j
  let J := numberFieldEmbeddedTopSubgroup K N j
  let hJH := numberFieldEmbeddedTopSubgroup_le_baseSubgroup K N j
  let hJH' : J.toSubgroup ≤ H'.toSubgroup :=
    numberFieldEmbeddedTopSubgroup_le_baseSubgroup M N j
  let hH'H := numberFieldEmbeddedBaseSubgroup_le_of_commonTop K M N j
  let lower := extensionSubgroup H J hJH
  let intermediate := extensionSubgroup H H' hH'H
  have hle : lower ≤ intermediate := by
    intro sigma hsigma
    rw [mem_extensionSubgroup_iff] at hsigma ⊢
    exact hJH' hsigma
  let : Finite (H.toSubgroup ⧸ lower) := by
    exact numberFieldEmbeddedExtensionQuotient_finite K N j
  let : lower.FiniteIndex :=
    Subgroup.finiteIndex_of_finite_quotient
  let : intermediate.FiniteIndex :=
    Subgroup.finiteIndex_of_le hle
  exact Subgroup.finite_quotient_of_finiteIndex

def
    numberFieldEmbeddedAbelianizedExtensionQuotientEquivGaloisAbelianization
    [FiniteDimensional K N] [IsGalois K N]
    (j : N →ₐ[ℚ] SeparableClosure ℚ) :
    Additive
        (Abelianization
          (numberFieldEmbeddedFiniteGaloisSubextension K N j).extensionQuotient) ≃+
      Additive (Abelianization Gal(N / K))

def
    numberFieldEmbeddedAbstractNormResidueGaloisAbelianizationEquiv
    [FiniteDimensional K N] [IsGalois K N]
    (j : N →ₐ[ℚ] SeparableClosure ℚ)
    [hRelativeFinite : Finite
      ((numberFieldEmbeddedBaseSubgroup K N j).toSubgroup ⧸
        extensionSubgroup
          (numberFieldEmbeddedBaseSubgroup K N j)
          (numberFieldEmbeddedTopSubgroup K N j)
          (numberFieldEmbeddedTopSubgroup_le_baseSubgroup K N j))] :
    FiniteNormQuotient rationalIdeleClassRepresentation
        (numberFieldEmbeddedBaseSubgroup K N j)
        (numberFieldEmbeddedTopSubgroup K N j)
        (numberFieldEmbeddedTopSubgroup_le_baseSubgroup K N j) ≃+
      Additive (Abelianization Gal(N / K))

theorem
    numberFieldEmbeddedAbstractNormResidueGaloisAbelianizationEquiv_apply
    [FiniteDimensional K N] [IsGalois K N]
    (j : N →ₐ[ℚ] SeparableClosure ℚ)
    [hRelativeFinite : Finite
      ((numberFieldEmbeddedBaseSubgroup K N j).toSubgroup ⧸
        extensionSubgroup
          (numberFieldEmbeddedBaseSubgroup K N j)
          (numberFieldEmbeddedTopSubgroup K N j)
          (numberFieldEmbeddedTopSubgroup_le_baseSubgroup K N j))]
    (x : FiniteNormQuotient rationalIdeleClassRepresentation
      (numberFieldEmbeddedBaseSubgroup K N j)
      (numberFieldEmbeddedTopSubgroup K N j)
      (numberFieldEmbeddedTopSubgroup_le_baseSubgroup K N j)) :
    numberFieldEmbeddedAbstractNormResidueGaloisAbelianizationEquiv K N j x =
      numberFieldEmbeddedAbelianizedExtensionQuotientEquivGaloisAbelianization
        K N j
        (rationalCyclotomicDegreeData.normResidueSymbol
          rationalIdeleClassRepresentation
          rationalCyclotomicIdeleClassValuationData
          rationalIdeleClassRepresentation_satisfiesClassFieldAxiom
          (numberFieldEmbeddedFiniteAbstractField K N j)
          (numberFieldEmbeddedFiniteGaloisSubextension K N j) x)

def globalNormResidueAbelianizationMonoidHomOfEmbedding
    [FiniteDimensional K N] [IsGalois K N]
    (j : N →ₐ[ℚ] SeparableClosure ℚ) :
    IdeleClassGroup K →* Abelianization Gal(N / K)

theorem globalNormResidueAbelianizationMonoidHomOfEmbedding_apply
    [FiniteDimensional K N] [IsGalois K N]
    (j : N →ₐ[ℚ] SeparableClosure ℚ)
    (c : IdeleClassGroup K) :
    letI _ : Finite
        ((numberFieldEmbeddedBaseSubgroup K N j).toSubgroup ⧸
          extensionSubgroup
            (numberFieldEmbeddedBaseSubgroup K N j)
            (numberFieldEmbeddedTopSubgroup K N j)
            (numberFieldEmbeddedTopSubgroup_le_baseSubgroup K N j)) :=
      numberFieldEmbeddedExtensionQuotient_finite K N j
    globalNormResidueAbelianizationMonoidHomOfEmbedding K N j c =
      Additive.toMul
        (numberFieldEmbeddedAbelianizedExtensionQuotientEquivGaloisAbelianization
          K N j
          (rationalCyclotomicDegreeData.normResidueSymbol
            rationalIdeleClassRepresentation
            rationalCyclotomicIdeleClassValuationData
            rationalIdeleClassRepresentation_satisfiesClassFieldAxiom
            (numberFieldEmbeddedFiniteAbstractField K N j)
            (numberFieldEmbeddedFiniteGaloisSubextension K N j)
            (finiteNormClass rationalIdeleClassRepresentation
              (numberFieldEmbeddedBaseSubgroup K N j)
              (numberFieldEmbeddedTopSubgroup K N j)
              (numberFieldEmbeddedTopSubgroup_le_baseSubgroup K N j)
              (numberFieldEmbeddedIdeleClassEquivAmbientFixed
                K N j (Additive.ofMul c))))) := by
  dsimp only
  let hRelativeFinite : Finite
      ((numberFieldEmbeddedBaseSubgroup K N j).toSubgroup ⧸
        extensionSubgroup
          (numberFieldEmbeddedBaseSubgroup K N j)
          (numberFieldEmbeddedTopSubgroup K N j)
          (numberFieldEmbeddedTopSubgroup_le_baseSubgroup K N j)) :=
    numberFieldEmbeddedExtensionQuotient_finite K N j
  have hclass :=
    numberFieldEmbeddedFiniteNormQuotientEquivIdeleClassNormQuotient_ideleClass
      K N j c
  let x :
      FiniteNormQuotient rationalIdeleClassRepresentation
        (numberFieldEmbeddedBaseSubgroup K N j)
        (numberFieldEmbeddedTopSubgroup K N j)
        (numberFieldEmbeddedTopSubgroup_le_baseSubgroup K N j) :=
    finiteNormClass rationalIdeleClassRepresentation
      (numberFieldEmbeddedBaseSubgroup K N j)
      (numberFieldEmbeddedTopSubgroup K N j)
      (numberFieldEmbeddedTopSubgroup_le_baseSubgroup K N j)
      (numberFieldEmbeddedIdeleClassEquivAmbientFixed
        K N j (Additive.ofMul c))
  let q : Additive
      (IdeleClassGroup K ⧸ (_root_.ideleClassNorm K N).range) :=
    Additive.ofMul
      (QuotientGroup.mk' (_root_.ideleClassNorm K N).range c)
  have hclass' :
      numberFieldEmbeddedFiniteNormQuotientEquivIdeleClassNormQuotient
          K N j x = q :=
    hclass
  have htransport :
      (numberFieldEmbeddedFiniteNormQuotientEquivIdeleClassNormQuotient
          K N j).symm q = x := by
    exact
      (congrArg
        (numberFieldEmbeddedFiniteNormQuotientEquivIdeleClassNormQuotient
          K N j).symm hclass'.symm).trans
        ((numberFieldEmbeddedFiniteNormQuotientEquivIdeleClassNormQuotient
          K N j).symm_apply_apply x)
  calc
    globalNormResidueAbelianizationMonoidHomOfEmbedding K N j c =
        Additive.toMul
          (numberFieldEmbeddedAbstractNormResidueGaloisAbelianizationEquiv
            K N j (hRelativeFinite := hRelativeFinite)
            ((numberFieldEmbeddedFiniteNormQuotientEquivIdeleClassNormQuotient
              K N j).symm q)) := by
      rfl
    _ =
        Additive.toMul
          (numberFieldEmbeddedAbstractNormResidueGaloisAbelianizationEquiv
            K N j (hRelativeFinite := hRelativeFinite) x) :=
      congrArg
        (fun y =>
          Additive.toMul
            (numberFieldEmbeddedAbstractNormResidueGaloisAbelianizationEquiv
              K N j (hRelativeFinite := hRelativeFinite) y))
        htransport
    _ =
        Additive.toMul
          (numberFieldEmbeddedAbelianizedExtensionQuotientEquivGaloisAbelianization
            K N j
            (rationalCyclotomicDegreeData.normResidueSymbol
              rationalIdeleClassRepresentation
              rationalCyclotomicIdeleClassValuationData
              rationalIdeleClassRepresentation_satisfiesClassFieldAxiom
              (numberFieldEmbeddedFiniteAbstractField K N j)
              (numberFieldEmbeddedFiniteGaloisSubextension K N j) x)) := by
      exact congrArg Additive.toMul
        (numberFieldEmbeddedAbstractNormResidueGaloisAbelianizationEquiv_apply
          K N j (hRelativeFinite := hRelativeFinite) x)

theorem
    globalNormResidueAbelianizationMonoidHom_eq_ofEmbedding_standard
    [FiniteDimensional K N] [IsGalois K N] :
    globalNormResidueAbelianizationMonoidHom K N =
      globalNormResidueAbelianizationMonoidHomOfEmbedding K N
        (numberFieldSeparableClosureEmbedding N)

theorem
    numberFieldEmbeddedIdeleClassEquivAmbientFixed_relativeNorm_of_commonTop
    [FiniteDimensional K N] [IsGalois K N]
    (j : N →ₐ[ℚ] SeparableClosure ℚ)
    (c : IdeleClassGroup M) :
    letI _ : FiniteDimensional K M :=
      commonTopBaseIntermediateFiniteDimensional K M N
    let H := numberFieldEmbeddedBaseSubgroup K N j
    let H' := numberFieldEmbeddedBaseSubgroup M N j
    let hH'H := numberFieldEmbeddedBaseSubgroup_le_of_commonTop K M N j
    letI _ : Finite (rationalFixedFieldAbsoluteQuotient H) :=
      (numberFieldEmbeddedFiniteAbstractField K N j).finite
    letI _ : Finite
        (rationalFixedFieldRelativeQuotient H H' hH'H) :=
      numberFieldEmbeddedBaseChangeExtensionQuotient_finite_of_commonTop
        K M N j
    relativeNorm rationalIdeleClassRepresentation H H' hH'H
        (numberFieldEmbeddedIdeleClassEquivAmbientFixed
          M N j (Additive.ofMul c)) =
      numberFieldEmbeddedIdeleClassEquivAmbientFixed
        K N j
        (Additive.ofMul (_root_.ideleClassNorm K M c)) := by
  intro H H'
  let hH'H := numberFieldEmbeddedBaseSubgroup_le_of_commonTop K M N j
  let hHfinite : Finite (rationalFixedFieldAbsoluteQuotient H) := by
    exact (numberFieldEmbeddedFiniteAbstractField K N j).finite
  let hHH'finite : Finite
      (rationalFixedFieldRelativeQuotient H H' hH'H) :=
    numberFieldEmbeddedBaseChangeExtensionQuotient_finite_of_commonTop
      K M N j
  let F := abstractFixedField ℚ (SeparableClosure ℚ) H
  let E := abstractRelativeFixedField ℚ (SeparableClosure ℚ) hH'H
  let : NumberField F := by
    let : FiniteDimensional ℚ F :=
      abstractFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ) H hHfinite
    exact NumberField.of_module_finite ℚ F
  let : NumberField E := by
    let : FiniteDimensional F E :=
      abstractRelativeFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ) H H' hH'H hHfinite hHH'finite
    exact NumberField.of_module_finite F E
  let hE :
      E.restrictScalars ℚ =
        abstractFixedField ℚ (SeparableClosure ℚ) H' :=
    IntermediateField.extendScalars_restrictScalars
      (abstractFixedField_le ℚ (SeparableClosure ℚ) hH'H)
  let eRel :
      E ≃ₐ[ℚ] abstractFixedField ℚ (SeparableClosure ℚ) H' :=
    IntermediateField.equivOfEq hE
  let eK : K ≃ₐ[ℚ] F :=
    numberFieldEmbeddedAbstractBaseFieldEquiv K N j
  let eMBase :
      M ≃ₐ[ℚ] abstractFixedField ℚ (SeparableClosure ℚ) H' :=
    numberFieldEmbeddedAbstractBaseFieldEquiv M N j
  let eM : M ≃ₐ[ℚ] E := eMBase.trans eRel.symm
  have hcompat (x : K) :
      eM (algebraMap K M x) = algebraMap F E (eK x) := by
    apply eRel.injective
    apply Subtype.ext
    change
      j (algebraMap M N (algebraMap K M x)) =
        j (algebraMap K N x)
    rw [IsScalarTower.algebraMap_apply K M N]
  have hupper :
      rationalAbstractRelativeFixedFieldIdeleClassEquivFixed
          H H' hH'H
          (Additive.ofMul (ideleClassCongr eM c)) =
        numberFieldEmbeddedIdeleClassEquivAmbientFixed
          M N j (Additive.ofMul c) := by
    apply Subtype.ext
    exact rationalIdeleClassEquivFixed_transport_commonTop_val
      (hA := by change FiniteDimensional ℚ E; infer_instance)
      (hB := numberFieldEmbeddedAbstractFixedFieldFiniteDimensional M N j)
      hE eMBase c
  have hrelative :=
    rationalAbstractRelativeFixedFieldIdeleClassEquivFixed_relativeNorm_ofFiniteTower
      H H' hH'H
  unfold rationalAbstractRelativeFixedFieldNormStatement at hrelative
  have hrelativec := hrelative (ideleClassCongr eM c)
  change
    relativeNorm rationalIdeleClassRepresentation H H' hH'H
        (rationalAbstractRelativeFixedFieldIdeleClassEquivFixed
          H H' hH'H
          (Additive.ofMul (ideleClassCongr eM c))) =
      rationalAbstractFixedFieldIdeleClassEquivFixed H
        (Additive.ofMul
          (_root_.ideleClassNorm F E (ideleClassCongr eM c)))
    at hrelativec
  calc
    _ = relativeNorm rationalIdeleClassRepresentation H H' hH'H
        (rationalAbstractRelativeFixedFieldIdeleClassEquivFixed H H' hH'H
          (Additive.ofMul (ideleClassCongr eM c))) :=
      congrArg (relativeNorm rationalIdeleClassRepresentation H H' hH'H) hupper.symm
    _ = rationalAbstractFixedFieldIdeleClassEquivFixed H
        (Additive.ofMul (_root_.ideleClassNorm F E (ideleClassCongr eM c))) :=
      hrelativec
    _ = _ := by
      change
        rationalAbstractFixedFieldIdeleClassEquivFixed H
            (Additive.ofMul (_root_.ideleClassNorm F E (ideleClassCongr eM c))) =
          rationalAbstractFixedFieldIdeleClassEquivFixed H
            (Additive.ofMul (ideleClassCongr eK (_root_.ideleClassNorm K M c)))
      apply congrArg (rationalAbstractFixedFieldIdeleClassEquivFixed H)
      apply congrArg Additive.ofMul
      exact (ideleClassCongr_ideleClassNorm
        (K := K) (K' := F) (L := M) (L' := E) eK eM hcompat c).symm

theorem
    numberFieldEmbeddedAbelianizedExtensionQuotientEquivGaloisAbelianization_restriction
    [FiniteDimensional K N] [IsGalois K N]
    (j : N →ₐ[ℚ] SeparableClosure ℚ) :
    letI _ : FiniteDimensional K M :=
      commonTopBaseIntermediateFiniteDimensional K M N
    letI _ : FiniteDimensional M N :=
      commonTopIntermediateTopFiniteDimensional K M N
    letI _ : IsGalois M N :=
      commonTopIntermediateTopIsGalois K M N
    ∀ z : Abelianization
        (numberFieldEmbeddedFiniteGaloisSubextension M N j).extensionQuotient,
    let H := numberFieldEmbeddedBaseSubgroup K N j
    let H' := numberFieldEmbeddedBaseSubgroup M N j
    let J := numberFieldEmbeddedTopSubgroup K N j
    let hJH := numberFieldEmbeddedTopSubgroup_le_baseSubgroup K N j
    let hJH' : J.toSubgroup ≤ H'.toSubgroup :=
      numberFieldEmbeddedTopSubgroup_le_baseSubgroup M N j
    let hH'H := numberFieldEmbeddedBaseSubgroup_le_of_commonTop K M N j
    letI _ : (extensionSubgroup H J hJH).Normal :=
      numberFieldEmbeddedExtensionSubgroup_normal K N j
    letI _ : (extensionSubgroup H' J hJH').Normal :=
      numberFieldEmbeddedExtensionSubgroup_normal M N j
    Abelianization.map
        (AlgEquiv.restrictScalarsHom K : Gal(N / M) →* Gal(N / K))
        (Additive.toMul
          (numberFieldEmbeddedAbelianizedExtensionQuotientEquivGaloisAbelianization
            M N j (Additive.ofMul z))) =
      Additive.toMul
        (numberFieldEmbeddedAbelianizedExtensionQuotientEquivGaloisAbelianization
          K N j
          (MonoidHom.toAdditive
            (normResidueNaturalityAbelianizedRestriction
              H H' J J hJH hJH' hH'H le_rfl)
            (Additive.ofMul z))) := by
  dsimp only
  let : FiniteDimensional K M :=
    commonTopBaseIntermediateFiniteDimensional K M N
  let : FiniteDimensional M N :=
    commonTopIntermediateTopFiniteDimensional K M N
  let : IsGalois M N :=
    commonTopIntermediateTopIsGalois K M N
  intro z
  let H := numberFieldEmbeddedBaseSubgroup K N j
  let H' := numberFieldEmbeddedBaseSubgroup M N j
  let J := numberFieldEmbeddedTopSubgroup K N j
  let hJH := numberFieldEmbeddedTopSubgroup_le_baseSubgroup K N j
  let hJH' : J.toSubgroup ≤ H'.toSubgroup :=
    numberFieldEmbeddedTopSubgroup_le_baseSubgroup M N j
  let hH'H := numberFieldEmbeddedBaseSubgroup_le_of_commonTop K M N j
  let hLowerNormal : (extensionSubgroup H J hJH).Normal :=
    numberFieldEmbeddedExtensionSubgroup_normal K N j
  let hUpperNormal : (extensionSubgroup H' J hJH').Normal :=
    numberFieldEmbeddedExtensionSubgroup_normal M N j
  let qLowerRaw :
      (H.toSubgroup ⧸ extensionSubgroup H J hJH) ≃* Gal(N / K) :=
    numberFieldEmbeddedExtensionQuotientEquivGaloisGroup K N j
  let qUpperRaw :
      (H'.toSubgroup ⧸ extensionSubgroup H' J hJH') ≃* Gal(N / M) :=
    numberFieldEmbeddedExtensionQuotientEquivGaloisGroup M N j
  let restrictActual : Gal(N / M) →* Gal(N / K) :=
    AlgEquiv.restrictScalarsHom K
  obtain ⟨q, rfl⟩ := QuotientGroup.mk_surjective z
  obtain ⟨sigma, rfl⟩ :=
    (numberFieldEmbeddedFiniteGaloisSubextension M N j).extensionQuotientMk_surjective q
  change
    Abelianization.map restrictActual
        (qUpperRaw.abelianizationCongr
          (Abelianization.of (QuotientGroup.mk sigma))) =
      qLowerRaw.abelianizationCongr
        (normResidueNaturalityAbelianizedRestriction
          H H' J J hJH hJH' hH'H le_rfl
          (Abelianization.of (QuotientGroup.mk sigma)))
  rw [normResidueNaturalityAbelianizedRestriction_of_mk,
    abelianizationCongr_of, abelianizationCongr_of,
    Abelianization.map_of]
  have hraw :
      restrictActual (qUpperRaw (QuotientGroup.mk sigma)) =
        qLowerRaw
          (QuotientGroup.mk (Subgroup.inclusion hH'H sigma)) := by
    apply AlgEquiv.ext
    intro x
    apply j.injective
    let hUpperAlgebra : Algebra M (SeparableClosure ℚ) :=
      numberFieldEmbeddedSeparableClosureAlgebra M N j
    let eUpper := numberFieldEmbeddedSeparableClosureEquiv M N j
    let hLowerAlgebra : Algebra K (SeparableClosure ℚ) :=
      numberFieldEmbeddedSeparableClosureAlgebra K N j
    let eLower := numberFieldEmbeddedSeparableClosureEquiv K N j
    calc
      j (restrictActual (qUpperRaw (QuotientGroup.mk sigma)) x) =
          sigma.1.1 (j x) := by
        exact
          ambientEmbeddedExtensionQuotientEquivGaloisGroup_mk_apply
            ℚ M N j eUpper sigma x
      _ = (Subgroup.inclusion hH'H sigma).1.1 (j x) := rfl
      _ = j
          (qLowerRaw
            (QuotientGroup.mk (Subgroup.inclusion hH'H sigma)) x) := by
        exact
          (ambientEmbeddedExtensionQuotientEquivGaloisGroup_mk_apply
            ℚ K N j eLower (Subgroup.inclusion hH'H sigma) x).symm
  exact congrArg Abelianization.of hraw

theorem
    globalNormResidueAbelianizationMonoidHomOfEmbedding_norm_restriction
    [FiniteDimensional K N] [IsGalois K N]
    (j : N →ₐ[ℚ] SeparableClosure ℚ) :
    letI _ : FiniteDimensional K M :=
      commonTopBaseIntermediateFiniteDimensional K M N
    letI _ : FiniteDimensional M N :=
      commonTopIntermediateTopFiniteDimensional K M N
    letI _ : IsGalois M N :=
      commonTopIntermediateTopIsGalois K M N
    (Abelianization.map
        (AlgEquiv.restrictScalarsHom K : Gal(N / M) →* Gal(N / K))).comp
        (globalNormResidueAbelianizationMonoidHomOfEmbedding M N j) =
      (globalNormResidueAbelianizationMonoidHomOfEmbedding K N j).comp
        (_root_.ideleClassNorm K M) := by
  let : FiniteDimensional K M :=
    commonTopBaseIntermediateFiniteDimensional K M N
  let : FiniteDimensional M N :=
    commonTopIntermediateTopFiniteDimensional K M N
  let : IsGalois M N :=
    commonTopIntermediateTopIsGalois K M N
  let H := numberFieldEmbeddedBaseSubgroup K N j
  let H' := numberFieldEmbeddedBaseSubgroup M N j
  let J := numberFieldEmbeddedTopSubgroup K N j
  let hJH := numberFieldEmbeddedTopSubgroup_le_baseSubgroup K N j
  let hJH' : J.toSubgroup ≤ H'.toSubgroup :=
    numberFieldEmbeddedTopSubgroup_le_baseSubgroup M N j
  let hH'H := numberFieldEmbeddedBaseSubgroup_le_of_commonTop K M N j
  let hLowerNormal : (extensionSubgroup H J hJH).Normal :=
    numberFieldEmbeddedExtensionSubgroup_normal K N j
  let hLowerFinite :
      Finite (H.toSubgroup ⧸ extensionSubgroup H J hJH) :=
    numberFieldEmbeddedExtensionQuotient_finite K N j
  let hUpperNormal : (extensionSubgroup H' J hJH').Normal :=
    numberFieldEmbeddedExtensionSubgroup_normal M N j
  let hUpperFinite :
      Finite (H'.toSubgroup ⧸ extensionSubgroup H' J hJH') :=
    numberFieldEmbeddedExtensionQuotient_finite M N j
  let hHH'finite :=
    numberFieldEmbeddedBaseChangeExtensionQuotient_finite_of_commonTop
      K M N j
  let T :
      FiniteAbstractFieldExtension
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ) :=
    { field := numberFieldEmbeddedFiniteAbstractField M N j
      base := numberFieldEmbeddedFiniteAbstractField K N j
      below := hH'H
      finiteQuotient := hHH'finite }
  let hTBaseNormal :
      (extensionSubgroup T.base.field J hJH).Normal := by
    change (extensionSubgroup H J hJH).Normal
    exact hLowerNormal
  let hTBaseFinite :
      Finite
        (T.base.field.toSubgroup ⧸
          extensionSubgroup T.base.field J hJH) := by
    change Finite (H.toSubgroup ⧸ extensionSubgroup H J hJH)
    exact hLowerFinite
  let hTFieldNormal :
      (extensionSubgroup T.field.field J hJH').Normal := by
    change (extensionSubgroup H' J hJH').Normal
    exact hUpperNormal
  let hTFieldFinite :
      Finite
        (T.field.field.toSubgroup ⧸
          extensionSubgroup T.field.field J hJH') := by
    change Finite (H'.toSubgroup ⧸ extensionSubgroup H' J hJH')
    exact hUpperFinite
  let restrictActual : Gal(N / M) →* Gal(N / K) :=
    AlgEquiv.restrictScalarsHom K
  apply MonoidHom.ext
  intro c
  let a :=
    numberFieldEmbeddedIdeleClassEquivAmbientFixed
      M N j (Additive.ofMul c)
  have hnat :=
    DegreeData.normResidueNaturality_norm_restriction
      (D := rationalCyclotomicDegreeData)
      (A := rationalIdeleClassRepresentation)
      (v := rationalCyclotomicIdeleClassValuationData)
      (hcf := rationalIdeleClassRepresentation_satisfiesClassFieldAxiom)
      (T := T) (L := J) (L' := J)
      (hLnormal := hTBaseNormal)
      (hL'normal := hTFieldNormal)
      (hLKfinite := hTBaseFinite)
      (hL'K'finite := hTFieldFinite)
      hJH hJH' le_rfl
  have hnatc :=
    DFunLike.congr_fun hnat
      (finiteNormClass rationalIdeleClassRepresentation
        H' J hJH' a)
  change _ =
    rationalCyclotomicDegreeData.normResidueSymbol
      rationalIdeleClassRepresentation
      rationalCyclotomicIdeleClassValuationData
      rationalIdeleClassRepresentation_satisfiesClassFieldAxiom
      T.base
      { field := J
        below := hJH
        normal := hTBaseNormal
        finite := hTBaseFinite }
      (finiteReciprocityNaturalityNormMap
        rationalIdeleClassRepresentation
        T.base.field T.field.field J J
        hJH hJH' T.below le_rfl
        (finiteNormClass rationalIdeleClassRepresentation
          T.field.field J hJH' a)) at hnatc
  rw [finiteReciprocityNaturalityNormMap_finiteNormClass] at hnatc
  have hnorm :
      relativeNorm rationalIdeleClassRepresentation H H' hH'H a =
        numberFieldEmbeddedIdeleClassEquivAmbientFixed K N j
          (Additive.ofMul (_root_.ideleClassNorm K M c)) :=
    numberFieldEmbeddedIdeleClassEquivAmbientFixed_relativeNorm_of_commonTop
      K M N j c
  calc
    Abelianization.map restrictActual
        (globalNormResidueAbelianizationMonoidHomOfEmbedding M N j c) =
      Abelianization.map restrictActual
        (Additive.toMul
          (numberFieldEmbeddedAbelianizedExtensionQuotientEquivGaloisAbelianization
            M N j
            (rationalCyclotomicDegreeData.normResidueSymbol
              rationalIdeleClassRepresentation
              rationalCyclotomicIdeleClassValuationData
              rationalIdeleClassRepresentation_satisfiesClassFieldAxiom
              (numberFieldEmbeddedFiniteAbstractField M N j)
              (numberFieldEmbeddedFiniteGaloisSubextension M N j)
              (finiteNormClass rationalIdeleClassRepresentation
                H' J hJH' a)))) := by
      rw [globalNormResidueAbelianizationMonoidHomOfEmbedding_apply]
    _ =
      Additive.toMul
        (numberFieldEmbeddedAbelianizedExtensionQuotientEquivGaloisAbelianization
          K N j
          (MonoidHom.toAdditive
            (normResidueNaturalityAbelianizedRestriction
              H H' J J hJH hJH' hH'H le_rfl)
            (rationalCyclotomicDegreeData.normResidueSymbol
              rationalIdeleClassRepresentation
              rationalCyclotomicIdeleClassValuationData
              rationalIdeleClassRepresentation_satisfiesClassFieldAxiom
              (numberFieldEmbeddedFiniteAbstractField M N j)
              (numberFieldEmbeddedFiniteGaloisSubextension M N j)
              (finiteNormClass rationalIdeleClassRepresentation
                H' J hJH' a)))) := by
      exact
        numberFieldEmbeddedAbelianizedExtensionQuotientEquivGaloisAbelianization_restriction
          K M N j _
    _ =
      Additive.toMul
        (numberFieldEmbeddedAbelianizedExtensionQuotientEquivGaloisAbelianization
          K N j
          (rationalCyclotomicDegreeData.normResidueSymbol
            rationalIdeleClassRepresentation
            rationalCyclotomicIdeleClassValuationData
            rationalIdeleClassRepresentation_satisfiesClassFieldAxiom
            (numberFieldEmbeddedFiniteAbstractField K N j)
            (numberFieldEmbeddedFiniteGaloisSubextension K N j)
            (finiteNormClass rationalIdeleClassRepresentation
              H J hJH
              (relativeNorm rationalIdeleClassRepresentation
                H H' hH'H a)))) := by
      exact congrArg
        (fun z =>
          Additive.toMul
            (numberFieldEmbeddedAbelianizedExtensionQuotientEquivGaloisAbelianization
              K N j z))
        hnatc
    _ =
      globalNormResidueAbelianizationMonoidHomOfEmbedding K N j
        (_root_.ideleClassNorm K M c) := by
      rw [hnorm,
        ← globalNormResidueAbelianizationMonoidHomOfEmbedding_apply]

theorem globalNormResidueAbelianizationMonoidHom_norm_restriction
    [FiniteDimensional K N] [IsGalois K N] :
    letI _ : FiniteDimensional K M :=
      commonTopBaseIntermediateFiniteDimensional K M N
    letI _ : FiniteDimensional M N :=
      commonTopIntermediateTopFiniteDimensional K M N
    letI _ : IsGalois M N :=
      commonTopIntermediateTopIsGalois K M N
    (Abelianization.map
        (AlgEquiv.restrictScalarsHom K : Gal(N / M) →* Gal(N / K))).comp
        (globalNormResidueAbelianizationMonoidHom M N) =
      (globalNormResidueAbelianizationMonoidHom K N).comp
        (_root_.ideleClassNorm K M) := by
  let : FiniteDimensional K M :=
    commonTopBaseIntermediateFiniteDimensional K M N
  let : FiniteDimensional M N :=
    commonTopIntermediateTopFiniteDimensional K M N
  let : IsGalois M N :=
    commonTopIntermediateTopIsGalois K M N
  rw [globalNormResidueAbelianizationMonoidHom_eq_ofEmbedding_standard,
    globalNormResidueAbelianizationMonoidHom_eq_ofEmbedding_standard]
  exact
    globalNormResidueAbelianizationMonoidHomOfEmbedding_norm_restriction
      K M N (numberFieldSeparableClosureEmbedding N)