GeneralTowerNaturality.lean

abbrev towerAbsoluteGalois (K : Type) [Field K]

abbrev towerAbsoluteUnits (K : Type) [Field K] :
    Rep ℤ (towerAbsoluteGalois K)

abbrev towerAbstractBase (K : Type) [Field K] :
    ClosedSubgroup (towerAbsoluteGalois K)

def towerLowerEmbedding
    (K E L : Type)
    [Field K] [Field E] [Field L]
    [Algebra K E] [Algebra E L] [Algebra K L]
    [IsScalarTower K E L]
    (iL : L →ₐ[K] SeparableClosure K) :
    E →ₐ[K] SeparableClosure K

def towerEmbeddedBaseNormClass
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (i : L →ₐ[K] SeparableClosure K) (a : Kˣ) :
    FiniteNormQuotient (towerAbsoluteUnits K) (towerAbstractBase K)
      (finiteGaloisAbstractExtensionOfEmbedding K L i).field
      (finiteGaloisAbstractExtensionOfEmbedding K L i).below

theorem towerEmbeddedFieldRange_le
    (K E L : Type)
    [Field K] [Field E] [Field L]
    [Algebra K E] [Algebra E L] [Algebra K L]
    [IsScalarTower K E L]
    (iL : L →ₐ[K] SeparableClosure K) :
    AlgHom.fieldRange (towerLowerEmbedding K E L iL) ≤
      AlgHom.fieldRange iL

theorem towerEmbeddedAbstractExtension_field_le
    (K E L : Type)
    [Field K] [Field E] [Field L]
    [Algebra K E] [Algebra E L] [Algebra K L]
    [IsScalarTower K E L]
    [FiniteDimensional K E] [FiniteDimensional K L]
    [IsGalois K E] [IsGalois K L]
    (iL : L →ₐ[K] SeparableClosure K) :
    (finiteGaloisAbstractExtensionOfEmbedding K L iL).field.toSubgroup ≤
      (finiteGaloisAbstractExtensionOfEmbedding K E
        (towerLowerEmbedding K E L iL)).field.toSubgroup

theorem towerRestrict_abstractQuotient_mk
    (K E L : Type)
    [Field K] [Field E] [Field L]
    [Algebra K E] [Algebra E L] [Algebra K L]
    [IsScalarTower K E L]
    [FiniteDimensional K E] [FiniteDimensional K L]
    [IsGalois K E] [IsGalois K L]
    (iL : L →ₐ[K] SeparableClosure K)
    (sigma : (towerAbstractBase K).toSubgroup) :
    AlgEquiv.restrictNormalHom E
        (finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding
          K L iL (QuotientGroup.mk sigma)) =
      finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding
        K E (towerLowerEmbedding K E L iL)
        (QuotientGroup.mk (Subgroup.inclusion le_rfl sigma))

theorem towerRestrict_abstractAbelianization
    (K E L : Type)
    [Field K] [Field E] [Field L]
    [Algebra K E] [Algebra E L] [Algebra K L]
    [IsScalarTower K E L]
    [FiniteDimensional K E] [FiniteDimensional K L]
    [IsAbelianGalois K E] [IsAbelianGalois K L]
    (iL : L →ₐ[K] SeparableClosure K)
    (z : Abelianization
      (finiteGaloisAbstractExtensionOfEmbedding K L iL).extensionQuotient) :
    AlgEquiv.restrictNormalHom E
        ((Abelianization.equivOfComm (H := Gal(L / K))).symm
          ((finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding
            K L iL).abelianizationCongr z)) =
      (Abelianization.equivOfComm (H := Gal(E / K))).symm
        ((finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding
          K E (towerLowerEmbedding K E L iL)).abelianizationCongr
          (normResidueNaturalityAbelianizedRestriction
            (towerAbstractBase K) (towerAbstractBase K)
            (finiteGaloisAbstractExtensionOfEmbedding
              K E (towerLowerEmbedding K E L iL)).field
            (finiteGaloisAbstractExtensionOfEmbedding K L iL).field
            (finiteGaloisAbstractExtensionOfEmbedding
              K E (towerLowerEmbedding K E L iL)).below
            (finiteGaloisAbstractExtensionOfEmbedding K L iL).below
            le_rfl (towerEmbeddedAbstractExtension_field_le K E L iL) z))

theorem concreteNormResidueAutomorphism_restrict_tower
    (K E L : Type)
    [Field K] [Field E] [Field L]
    [Algebra K E] [Algebra E L] [Algebra K L]
    [IsScalarTower K E L]
    [FiniteDimensional K E] [FiniteDimensional K L]
    [IsAbelianGalois K E] [IsAbelianGalois K L]
    (iL : L →ₐ[K] SeparableClosure K)
    (D : DegreeData (towerAbsoluteGalois K))
    (v : ValuationData D (towerAbsoluteUnits K))
    (hcf : SatisfiesClassFieldAxiom (towerAbsoluteUnits K))
    (a : Kˣ) :
    AlgEquiv.restrictNormalHom E
        ((Abelianization.equivOfComm (H := Gal(L / K))).symm
          (concreteNormResidueSymbolOfEmbedding
            K L iL D v hcf a)) =
      (Abelianization.equivOfComm (H := Gal(E / K))).symm
        (concreteNormResidueSymbolOfEmbedding
          K E (towerLowerEmbedding K E L iL) D v hcf a)

theorem localArtinAutomorphism_restrict_tower
    (K E L : Type)
    [Field K] [Field E] [Field L]
    [Algebra K E] [Algebra E L] [Algebra K L]
    [IsScalarTower K E L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K E] [FiniteDimensional K L]
    [IsAbelianGalois K E] [IsAbelianGalois K L]
    (a : Kˣ) :
    AlgEquiv.restrictNormalHom E
        ((Abelianization.equivOfComm (H := Gal(L / K))).symm
          (localArtinMonoidHom K L a)) =
      (Abelianization.equivOfComm (H := Gal(E / K))).symm
        (localArtinMonoidHom K E a)

theorem abelianLocalArtinMonoidHom_restrict_tower
    (K E L : Type)
    [Field K] [Field E] [Field L]
    [Algebra K E] [Algebra E L] [Algebra K L]
    [IsScalarTower K E L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K E] [FiniteDimensional K L]
    [IsAbelianGalois K E] [IsAbelianGalois K L] :
    (AlgEquiv.restrictNormalHom E).comp
        (abelianLocalArtinMonoidHom K L) =
      abelianLocalArtinMonoidHom K E

theorem restrictNormalHom_eq_autCongr
    (K L M : Type)
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    [Normal K M]
    (e : L ≃ₐ[K] M) :
    letI : Algebra M L := e.symm.toRingHom.toAlgebra
    letI : IsScalarTower K M L :=
      IsScalarTower.of_algebraMap_eq' (by
        apply RingHom.ext
        intro x
        exact (e.symm.commutes x).symm)
    (AlgEquiv.restrictNormalHom M :
        Gal(L / K) →* Gal(M / K)) =
      (AlgEquiv.autCongr e).toMonoidHom := by
  let : Algebra M L := e.symm.toRingHom.toAlgebra
  let : IsScalarTower K M L :=
    IsScalarTower.of_algebraMap_eq' (by
      apply RingHom.ext
      intro x
      exact (e.symm.commutes x).symm)
  apply MonoidHom.ext
  intro sigma
  apply AlgEquiv.ext
  intro x
  apply e.symm.injective
  calc
    e.symm ((AlgEquiv.restrictNormalHom M sigma) x) =
        sigma (e.symm x) := by
      exact AlgEquiv.restrictNormal_commutes sigma M x
    _ = e.symm ((AlgEquiv.autCongr e sigma) x) := by
      simp [AlgEquiv.autCongr_apply]

theorem abelianLocalArtinMonoidHom_autCongr
    (K L M : Type)
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsAbelianGalois K L] [IsAbelianGalois K M]
    (e : L ≃ₐ[K] M) :
    (AlgEquiv.autCongr e).toMonoidHom.comp
        (abelianLocalArtinMonoidHom K L) =
      abelianLocalArtinMonoidHom K M

theorem finiteAbelianLocalArtinMap_restrict_tower
    (K E L : Type)
    [Field K] [Field E] [Field L]
    [Algebra K E] [Algebra E L] [Algebra K L]
    [IsScalarTower K E L]
    [FiniteDimensional K E] [FiniteDimensional K L]
    [IsAbelianGalois K E] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    (AlgEquiv.restrictNormalHom E).comp
        (LocalClassFieldTheory.abelianLocalArtinMap K L).toMonoidHom =
      (LocalClassFieldTheory.abelianLocalArtinMap K E).toMonoidHom