IdeleClassDirectLimitFiniteTowerNormCore.lean

theorem finiteTowerIdeleIsMulCommutative
    {K M L : Type u}
    [Field K] [NumberField K] [Field M] [Field L]
    [Algebra K M] [Algebra M L] :
    IsMulCommutative (TowerRelativeIdeleGroup K M L)

def normalClosureAlgHomEquiv
    {F E L : Type u}
    [Field F] [Field E] [Field L]
    [Algebra F E] [Algebra F L] :
    (E →ₐ[F] L) ≃
      (E →ₐ[F] IntermediateField.normalClosure F E L)

def normalClosureLiftAlgHom
    {F E L : Type u}
    [Field F] [Field E] [Field L]
    [Algebra F E] [Algebra F L]
    (f : E →ₐ[F] L) :
    E →ₐ[F] IntermediateField.normalClosure F E L

def algHomOfCompatibleRingHom
    {R S A : Type u}
    [CommSemiring R] [CommSemiring S] [Semiring A]
    [Algebra R S] [Algebra R A]
    (f : S →+* A)
    (h : ∀ x : R, f (algebraMap R S x) = algebraMap R A x) :
    S →ₐ[R] A where
  toRingHom := f
  commutes' := h

theorem relativeAdeleEmbedding_toAlgHom_unflatten
    {K M L : Type u}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    (a : RelativeAdeleRing K M) :
    towerRelativeAdeleUnflatten K M L
        (RelativeIdeleGroup.adeleEmbedding
          (IsScalarTower.toAlgHom K M L) a) =
      a ⊗ₜ[M] (1 : L)

theorem relativeIdeleEmbedding_toAlgHom_unflatten
    {K M L : Type u}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    (a : RelativeIdeleGroup K M) :
    letI : Algebra M (RelativeAdeleRing K M) :=
      relativeAdeleRingIntermediateAlgebra K M
    (towerRelativeIdeleEquiv K M L).symm
        (RelativeIdeleGroup.ideleEmbedding
          (IsScalarTower.toAlgHom K M L) a) =
      (Units.map
        (@Algebra.TensorProduct.includeLeft
          M M (RelativeAdeleRing K M) L
          inferInstance inferInstance
          (relativeAdeleRingIntermediateAlgebra K M)
          inferInstance inferInstance inferInstance
          (relativeAdeleRingIntermediateAlgebra K M)
          (smulCommClass_self M (RelativeAdeleRing K M))).toRingHom a :
        TowerRelativeIdeleGroup K M L) := by
  let _ : Algebra M (RelativeAdeleRing K M) :=
    relativeAdeleRingIntermediateAlgebra K M
  apply Units.ext
  exact relativeAdeleEmbedding_toAlgHom_unflatten
    (K := K) (M := M) (L := L) (a : RelativeAdeleRing K M)

theorem
    relativeIdeleClassEmbedding_toAlgHom_towerBaseChange
    {K M L : Type u}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    (c : RelativeIdeleGroup.ClassGroup K M) :
    towerRelativeIdeleClassBaseChangeMulEquiv K M L
        ((TowerRelativeIdeleGroup.classGroupEquiv K M L).symm
          (RelativeIdeleGroup.classEmbedding
            (IsScalarTower.toAlgHom K M L) c)) =
      RelativeIdeleGroup.classInclusion M L
        (_root_.relativeIdeleClassBaseChangeMulEquiv
          (K := K) (L := M) c)

theorem
    relativeIdeleClassBaseChange_classEmbedding_toAlgHom
    {K M L : Type u}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    (c : RelativeIdeleGroup.ClassGroup K M) :
    _root_.relativeIdeleClassBaseChangeMulEquiv
        (K := K) (L := L)
        (RelativeIdeleGroup.classEmbedding
          (IsScalarTower.toAlgHom K M L) c) =
      _root_.ideleClassExtension M L
        (_root_.relativeIdeleClassBaseChangeMulEquiv
          (K := K) (L := M) c)

theorem classEmbedding_smul_eq_classEmbedding_comp
    {K E U : Type u}
    [Field K] [NumberField K]
    [Field E] [Field U]
    [Algebra K E] [Algebra K U]
    [FiniteDimensional K E] [FiniteDimensional K U]
    (j : E →ₐ[K] U) (σ : U ≃ₐ[K] U)
    (c : RelativeIdeleGroup.ClassGroup K E) :
    σ • RelativeIdeleGroup.classEmbedding j c =
      RelativeIdeleGroup.classEmbedding (σ.toAlgHom.comp j) c

theorem classEmbedding_changeBase
    {k F E U : Type u}
    [Field k] [NumberField k]
    [Field F] [NumberField F]
    [Field E] [NumberField E]
    [Field U] [NumberField U]
    [Algebra k F] [Algebra F E] [Algebra k E]
    [Algebra E U] [Algebra F U] [Algebra k U]
    [IsScalarTower k F E] [IsScalarTower F E U]
    [IsScalarTower k F U] [IsScalarTower k E U]
    [FiniteDimensional k F] [FiniteDimensional F E]
    [FiniteDimensional E U] [FiniteDimensional F U]
    [IsGalois F U]
    (f : E →ₐ[F] U) (c : IdeleClassGroup E) :
    towerRelativeIdeleClassBaseChangeMulEquiv k F U
        ((TowerRelativeIdeleGroup.classGroupEquiv k F U).symm
          (RelativeIdeleGroup.classEmbedding
            (f.restrictScalars k)
            ((_root_.relativeIdeleClassBaseChangeMulEquiv
              (K := k) (L := E)).symm c))) =
      RelativeIdeleGroup.classEmbedding f
        ((_root_.relativeIdeleClassBaseChangeMulEquiv
          (K := F) (L := E)).symm c)

theorem relativeIdeleClassBaseChange_classEmbedding_changeBase
    {k F E U : Type u}
    [Field k] [NumberField k]
    [Field F] [NumberField F]
    [Field E] [NumberField E]
    [Field U] [NumberField U]
    [Algebra k F] [Algebra F E] [Algebra k E]
    [Algebra E U] [Algebra F U] [Algebra k U]
    [IsScalarTower k F E] [IsScalarTower F E U]
    [IsScalarTower k F U] [IsScalarTower k E U]
    [FiniteDimensional k F] [FiniteDimensional F E]
    [FiniteDimensional E U] [FiniteDimensional F U]
    [IsGalois F U]
    (f : E →ₐ[F] U) (c : IdeleClassGroup E) :
    _root_.relativeIdeleClassBaseChangeMulEquiv
        (K := k) (L := U)
        (RelativeIdeleGroup.classEmbedding
          (f.restrictScalars k)
          ((_root_.relativeIdeleClassBaseChangeMulEquiv
            (K := k) (L := E)).symm c)) =
      _root_.relativeIdeleClassBaseChangeMulEquiv
        (K := F) (L := U)
        (RelativeIdeleGroup.classEmbedding f
          ((_root_.relativeIdeleClassBaseChangeMulEquiv
            (K := F) (L := E)).symm c))

theorem classEmbedding_comp
    {K E N U : Type u}
    [Field K] [NumberField K]
    [Field E] [Field N] [Field U]
    [Algebra K E] [Algebra K N] [Algebra K U]
    [FiniteDimensional K E] [FiniteDimensional K N]
    [FiniteDimensional K U]
    (f : E →ₐ[K] N) (g : N →ₐ[K] U)
    (c : RelativeIdeleGroup.ClassGroup K E) :
    RelativeIdeleGroup.classEmbedding g
        (RelativeIdeleGroup.classEmbedding f c) =
      RelativeIdeleGroup.classEmbedding (g.comp f) c

theorem relativeIdeleClassBaseChange_prod_embeddings
    {F E N U Q : Type u}
    [Field F] [NumberField F]
    [Field E] [Field N]
    [Field U] [NumberField U]
    [Algebra F E] [Algebra F N] [Algebra F U]
    [Algebra E N] [IsScalarTower F E N]
    [FiniteDimensional F E] [FiniteDimensional F N]
    [FiniteDimensional F U] [IsGalois F N]
    [Fintype Q]
    (e : Q ≃ (E →ₐ[F] N)) (j : N →ₐ[F] U)
    (c : RelativeIdeleGroup.ClassGroup F E) :
    (∏ q : Q,
      _root_.relativeIdeleClassBaseChangeMulEquiv
        (K := F) (L := U)
        (RelativeIdeleGroup.classEmbedding (j.comp (e q)) c)) =
      _root_.relativeIdeleClassBaseChangeMulEquiv
        (K := F) (L := U)
        (RelativeIdeleGroup.classEmbedding j
          (RelativeIdeleGroup.classInclusion F N
            (RelativeIdeleGroup.classNorm F E c)))

theorem
    rationalIntermediateIdeleClassToDirectLimit_classEmbedding
    (E : IntermediateField ℚ (SeparableClosure ℚ))
    (U : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ E]
    (hEU : E ≤ (U : IntermediateField ℚ (SeparableClosure ℚ)))
    (c : IdeleClassGroup E) :
    rationalIntermediateIdeleClassToDirectLimit E c =
      rationalRelativeIdeleClassToDirectLimit U
        (RelativeIdeleGroup.classEmbedding (K := ℚ) (L := E) (M := U)
          (IntermediateField.inclusion hEU)
          ((_root_.relativeIdeleClassBaseChangeMulEquiv
            (K := ℚ) (L := E)).symm c))