NYLL
Module

NormRestriction.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FixedFieldIntrinsicReciprocity.NormRestriction
4 declarations indexed from sourceView source ↗

Module documentation

Norm--restriction for local Artin maps

This module proves norm--restriction naturality for actual finite abelian local Artin maps.

Imports2
Imported by5

Declarations

theorem

quotientRestriction

L28 ↗
LocalClassFieldTheory.AmbientEmbeddedFixedFieldPresentation.quotientRestriction
Documentation

A compatible restriction of concrete embedded Galois actions induces the corresponding restriction map on ambient finite quotient representatives.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped IsMulCommutative ValuativeRel
Lean source · statement
theorem AmbientEmbeddedFixedFieldPresentation.quotientRestriction
    (K K' L L' : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field K'] [ValuativeRel K'] [TopologicalSpace K']
    [IsNonarchimedeanLocalField K']
    [Field L] [Field L']
    [Algebra K K'] [Algebra K L] [Algebra K L']
    [Algebra K' L'] [Algebra L L']
    [IsScalarTower K K' L'] [IsScalarTower K L L']
    [FiniteDimensional K K'] [Algebra.IsSeparable K K']
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation K')]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [FiniteDimensional K' L'] [IsAbelianGalois K' L']
    {jLower : L →ₐ[K] SeparableClosure K}
    {jUpper : L' →ₐ[K] SeparableClosure K}
    (lower : AmbientEmbeddedFixedFieldPresentation K K L jLower)
    (upper : AmbientEmbeddedFixedFieldPresentation K K' L' jUpper)
    (hH'H : upper.base.field.toSubgroup ≤ lower.base.field.toSubgroup)
    (hJ'J : upper.extension.field.toSubgroup ≤
      lower.extension.field.toSubgroup)
    [hJnormal :
      (extensionSubgroup lower.base.field lower.extension.field
        lower.extension.below).Normal]
    [_hJfinite : Finite
      (lower.base.field.toSubgroup ⧸
        extensionSubgroup lower.base.field lower.extension.field
          lower.extension.below)]
    [hJ'normal :
      (extensionSubgroup upper.base.field upper.extension.field
        upper.extension.below).Normal]
    [_hJ'finite : Finite
      (upper.base.field.toSubgroup ⧸
        extensionSubgroup upper.base.field upper.extension.field
          upper.extension.below)]
    [_hHabsolute : Finite
      ((baseField Gal(SeparableClosure K/K)).toSubgroup ⧸
        extensionSubgroup
          (baseField Gal(SeparableClosure K/K))
          lower.base.field (le_baseField lower.base.field))]
    [_hH'absolute : Finite
      ((baseField Gal(SeparableClosure K/K)).toSubgroup ⧸
        extensionSubgroup
          (baseField Gal(SeparableClosure K/K))
          upper.base.field (le_baseField upper.base.field))]
    [_hH'finite : Finite
      (lower.base.field.toSubgroup ⧸
        extensionSubgroup lower.base.field upper.base.field hH'H)]
    (restrictActual : Gal(L'/K') →* Gal(L/K))
    (hbase : ∀ x : L,
      jUpper (algebraMap L L' x) = jLower x)
    (hcompat : ∀ (τ : Gal(L' / K')) (x : L),
      jLower (restrictActual τ x) =
        jUpper (τ (algebraMap L L' x)))
    (z : Abelianization
      (upper.base.field.toSubgroup ⧸
        extensionSubgroup upper.base.field upper.extension.field
          upper.extension.below)) :
    restrictActual
        ((Abelianization.equivOfComm (H := Gal(L' / K'))).symm
          ((upper.extension.extensionQuotientMulEquiv.symm.trans
            upper.quotientEquiv).abelianizationCongr z)) =
      (Abelianization.equivOfComm (H := Gal(L / K))).symm
        ((lower.extension.extensionQuotientMulEquiv.symm.trans
          lower.quotientEquiv).abelianizationCongr
          (normResidueNaturalityAbelianizedRestriction
            lower.base.field upper.base.field
            lower.extension.field upper.extension.field
            lower.extension.below upper.extension.below
            hH'H hJ'J z))
theorem

fixedFieldNormResidueTransport

L190 ↗
LocalClassFieldTheory.AmbientEmbeddedFixedFieldPresentation.fixedFieldNormResidueTransport
Documentation

The actual abstract fixed-field norm-residue symbols commute with norm and restriction through the canonical quotient equivalences of the presentations.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped IsMulCommutative ValuativeRel
Lean source · statement
theorem AmbientEmbeddedFixedFieldPresentation.fixedFieldNormResidueTransport
    (K K' L L' : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field K'] [ValuativeRel K'] [TopologicalSpace K']
    [IsNonarchimedeanLocalField K']
    [Field L] [Field L']
    [Algebra K K'] [Algebra K L] [Algebra K L']
    [Algebra K' L'] [Algebra L L']
    [IsScalarTower K K' L'] [IsScalarTower K L L']
    [FiniteDimensional K K'] [Algebra.IsSeparable K K']
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation K')]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [FiniteDimensional K' L'] [IsAbelianGalois K' L']
    {jLower : L →ₐ[K] SeparableClosure K}
    {jUpper : L' →ₐ[K] SeparableClosure K}
    (lower : AmbientEmbeddedFixedFieldPresentation K K L jLower)
    (upper : AmbientEmbeddedFixedFieldPresentation K K' L' jUpper)
    (hH'H : upper.base.field.toSubgroup ≤ lower.base.field.toSubgroup)
    (hJ'J : upper.extension.field.toSubgroup ≤
      lower.extension.field.toSubgroup)
    [hJnormal :
      (extensionSubgroup lower.base.field lower.extension.field
        lower.extension.below).Normal]
    [_hJfinite : Finite
      (lower.base.field.toSubgroup ⧸
        extensionSubgroup lower.base.field lower.extension.field
          lower.extension.below)]
    [hJ'normal :
      (extensionSubgroup upper.base.field upper.extension.field
        upper.extension.below).Normal]
    [_hJ'finite : Finite
      (upper.base.field.toSubgroup ⧸
        extensionSubgroup upper.base.field upper.extension.field
          upper.extension.below)]
    [_hHabsolute : Finite
      ((baseField Gal(SeparableClosure K/K)).toSubgroup ⧸
        extensionSubgroup
          (baseField Gal(SeparableClosure K/K))
          lower.base.field (le_baseField lower.base.field))]
    [_hH'absolute : Finite
      ((baseField Gal(SeparableClosure K/K)).toSubgroup ⧸
        extensionSubgroup
          (baseField Gal(SeparableClosure K/K))
          upper.base.field (le_baseField upper.base.field))]
    [_hH'finite : Finite
      (lower.base.field.toSubgroup ⧸
        extensionSubgroup lower.base.field upper.base.field hH'H)]
    (hbase : ∀ x : L,
      jUpper (algebraMap L L' x) = jLower x)
    (a : K'ˣ) :
    normResidueNaturalityAbelianizedRestriction
        lower.base.field upper.base.field
        lower.extension.field upper.extension.field
        lower.extension.below upper.extension.below
        hH'H hJ'J
        ((upper.extension.extensionQuotientMulEquiv.symm.trans
          upper.fixedFieldQuotientEquiv).abelianizationCongr.symm
          (Additive.toMul
            (abstractFixedFieldNormResidueSymbol
              K (SeparableClosure K)
              (localResidueDatum K)
              (localHenselianValuation K)
              (separableClosureUnits_isClassFormation K)
              upper.base.field upper.extension.field
              upper.extension.below
              (Additive.ofMul
                (Units.mapEquiv upper.baseEquiv.toMulEquiv a))))) =
      (lower.extension.extensionQuotientMulEquiv.symm.trans
        lower.fixedFieldQuotientEquiv).abelianizationCongr.symm
        (Additive.toMul
          (abstractFixedFieldNormResidueSymbol
            K (SeparableClosure K)
            (localResidueDatum K)
            (localHenselianValuation K)
            (separableClosureUnits_isClassFormation K)
            lower.base.field lower.extension.field
            lower.extension.below
            (Additive.ofMul
              (Units.mapEquiv lower.baseEquiv.toMulEquiv
                (normUnits K K' a)))))
theorem

ambientEmbeddedNormResidueElement_norm_restriction

L393 ↗
LocalClassFieldTheory.ambientEmbeddedNormResidueElement_norm_restriction
Documentation

Canonical ambient fixed-field norm-residue values commute with restriction and norm in an arbitrary finite square of nonarchimedean local fields.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped IsMulCommutative ValuativeRel
Lean source · full declaration
theorem ambientEmbeddedNormResidueElement_norm_restriction
    (K K' L L' : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field K'] [ValuativeRel K'] [TopologicalSpace K']
    [IsNonarchimedeanLocalField K']
    [Field L] [Field L']
    [Algebra K K'] [Algebra K L] [Algebra K L']
    [Algebra K' L'] [Algebra L L']
    [IsScalarTower K K' L'] [IsScalarTower K L L']
    [FiniteDimensional K K'] [Algebra.IsSeparable K K']
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation K')]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [FiniteDimensional K' L'] [IsAbelianGalois K' L']
    (j : L' →ₐ[K] SeparableClosure K)
    (eLower :
      @AlgEquiv K (SeparableClosure K) (SeparableClosure K)
        _ _ _
        (separableClosure K (AlgebraicClosure K)).algebra
        (((j.comp (IsScalarTower.toAlgHom K L L')).comp
          (IsScalarTower.toAlgHom K K L)).toRingHom.toAlgebra))
    (eUpper :
      letI : Algebra K' (SeparableClosure K) :=
        (j.comp (IsScalarTower.toAlgHom K K' L')).toRingHom.toAlgebra
      SeparableClosure K' ≃ₐ[K'] SeparableClosure K)
    (a : K'ˣ) :
    ((AlgEquiv.restrictNormalHom L).comp
        (AlgEquiv.restrictScalarsHom K))
        (ambientEmbeddedNormResidueElement K K' L' j eUpper a) =
      ambientEmbeddedNormResidueElement K K L
        (j.comp (IsScalarTower.toAlgHom K L L')) eLower
        (normUnits K K' a) := by
  let : FiniteDimensional K L' :=
    FiniteDimensional.trans K K' L'
  let : Algebra.IsSeparable K L' :=
    Algebra.IsSeparable.trans K K' L'
  let iUpper : K' →ₐ[K] SeparableClosure K :=
    j.comp (IsScalarTower.toAlgHom K K' L')
  let jLower : L →ₐ[K] SeparableClosure K :=
    j.comp (IsScalarTower.toAlgHom K L L')
  let iLower : K →ₐ[K] SeparableClosure K :=
    jLower.comp (IsScalarTower.toAlgHom K K L)
  let lower :=
    ambientEmbeddedFixedFieldPresentation K K L jLower eLower
  let upper :=
    ambientEmbeddedFixedFieldPresentation K K' L' j eUpper
  let H := lower.base.field
  let H' := upper.base.field
  let J := lower.extension.field
  let J' := upper.extension.field
  have hRangeHH :
      AlgHom.fieldRange iLower ≤
        AlgHom.fieldRange iUpper := by
    intro x hx
    rcases hx with ⟨y, rfl⟩
    refine ⟨algebraMap K K' y, ?_⟩
    change
      j (algebraMap K' L' (algebraMap K K' y)) =
        j (algebraMap L L' (algebraMap K L y))
    rw [← IsScalarTower.algebraMap_apply K K' L',
      ← IsScalarTower.algebraMap_apply K L L']
  let hH'H : H'.toSubgroup ≤ H.toSubgroup := by
    change upper.base.field.toSubgroup ≤ lower.base.field.toSubgroup
    rw [lower.base_field_eq, upper.base_field_eq,
      lower.baseEmbedding_eq, upper.baseEmbedding_eq]
    change
      (AlgHom.fieldRange iUpper).fixingSubgroup ≤
        (AlgHom.fieldRange iLower).fixingSubgroup
    exact
      (AlgHom.fieldRange iLower).fixingSubgroup_le
        hRangeHH
  have hRangeJJ :
      AlgHom.fieldRange jLower ≤
        AlgHom.fieldRange j := by
    intro x hx
    rcases hx with ⟨y, rfl⟩
    exact ⟨algebraMap L L' y, rfl⟩
  let hJ'J : J'.toSubgroup ≤ J.toSubgroup := by
    change upper.extension.field.toSubgroup ≤ lower.extension.field.toSubgroup
    rw [lower.extension_field_eq, upper.extension_field_eq]
    change
      (AlgHom.fieldRange j).fixingSubgroup ≤
        (AlgHom.fieldRange jLower).fixingSubgroup
    exact
      (AlgHom.fieldRange jLower).fixingSubgroup_le
        hRangeJJ
  let hJH : J.toSubgroup ≤ H.toSubgroup := lower.extension.below
  let hJ'H' : J'.toSubgroup ≤ H'.toSubgroup := upper.extension.below
  let hJnormal :
      (extensionSubgroup H J hJH).Normal :=
    lower.extension.normal
  let hJfinite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H J hJH) :=
    lower.extension.finite
  let hJ'normal :
      (extensionSubgroup H' J' hJ'H').Normal :=
    upper.extension.normal
  let hJ'finite : Finite
      (H'.toSubgroup ⧸ extensionSubgroup H' J' hJ'H') :=
    upper.extension.finite
  let hHabsolute : Finite
      ((baseField
        Gal(SeparableClosure K / K)).toSubgroup ⧸
        extensionSubgroup
          (baseField Gal(SeparableClosure K / K))
          H (le_baseField H)) :=
    lower.base.finite
  let hH'absolute : Finite
      ((baseField
        Gal(SeparableClosure K / K)).toSubgroup ⧸
        extensionSubgroup
          (baseField Gal(SeparableClosure K / K))
          H' (le_baseField H')) :=
    upper.base.finite
  let hH'finite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H H' hH'H) := by
    let inclusion :=
      Subgroup.quotientSubgroupOfEmbeddingOfLE
        H'.toSubgroup (le_baseField H)
    exact Finite.of_injective inclusion inclusion.injective
  let FLower :=
    abstractFixedField K (SeparableClosure K) H
  let phiLower : K ≃ₐ[K] FLower :=
    lower.baseEquiv
  let FUpper :=
    abstractFixedField K (SeparableClosure K) H'
  let phiUpper : K' ≃ₐ[K] FUpper :=
    upper.baseEquiv
  let restrictActual :
      Gal(L' / K') →* Gal(L / K) :=
    (AlgEquiv.restrictNormalHom L).comp
      (AlgEquiv.restrictScalarsHom K)
  have hcompat : ∀ (τ : Gal(L' / K')) (x : L),
      jLower (restrictActual τ x) =
        j (τ (algebraMap L L' x)) := by
    intro τ x
    exact congrArg j
      (AlgEquiv.restrictNormal_commutes
        ((AlgEquiv.restrictScalarsHom K) τ) L x)
  have hbase : ∀ x : L,
      j (algebraMap L L' x) = jLower x := by
    intro x
    rfl
  let aUpper : FUpperˣ :=
    Units.mapEquiv phiUpper.toMulEquiv a
  let aNorm : Kˣ :=
    normUnits K K' a
  let aLower : FLowerˣ :=
    Units.mapEquiv phiLower.toMulEquiv aNorm
  let symbolUpper :=
    abstractFixedFieldNormResidueSymbol
      K (SeparableClosure K)
      (localResidueDatum K)
      (localHenselianValuation K)
      (separableClosureUnits_isClassFormation K)
      H' J' hJ'H'
  let symbolLower :=
    abstractFixedFieldNormResidueSymbol
      K (SeparableClosure K)
      (localResidueDatum K)
      (localHenselianValuation K)
      (separableClosureUnits_isClassFormation K)
      H J hJH
  let upperSymbolValue :=
    Additive.toMul
      (symbolUpper (Additive.ofMul aUpper))
  let lowerSymbolValue :=
    Additive.toMul
      (symbolLower (Additive.ofMul aLower))
  let upperQuotientValue :=
    upper.fixedFieldQuotientEquiv.abelianizationCongr.symm
      upperSymbolValue
  let lowerQuotientValue :=
    lower.fixedFieldQuotientEquiv.abelianizationCongr.symm
      lowerSymbolValue
  have hraw :
      normResidueNaturalityAbelianizedRestriction
          H H' J J' hJH hJ'H' hH'H hJ'J
          ((upper.extension.extensionQuotientMulEquiv.symm.trans
            upper.fixedFieldQuotientEquiv).abelianizationCongr.symm
            upperSymbolValue) =
        (lower.extension.extensionQuotientMulEquiv.symm.trans
          lower.fixedFieldQuotientEquiv).abelianizationCongr.symm
          lowerSymbolValue := by
    simpa only [H, H', J, J', hJH, hJ'H',
      aUpper, aLower, aNorm, symbolUpper, symbolLower,
      upperSymbolValue, lowerSymbolValue] using
      AmbientEmbeddedFixedFieldPresentation.fixedFieldNormResidueTransport
        K K' L L' lower upper hH'H hJ'J
        hbase a
  have htarget
      (z : Abelianization upper.extension.extensionQuotient) :
      restrictActual
          ((Abelianization.equivOfComm (H := Gal(L' / K'))).symm
            (upper.quotientEquiv.abelianizationCongr z)) =
        (Abelianization.equivOfComm (H := Gal(L / K))).symm
          (lower.quotientEquiv.abelianizationCongr
            (lower.extension.extensionQuotientMulEquiv.abelianizationCongr.symm
              (normResidueNaturalityAbelianizedRestriction
                H H' J J' hJH hJ'H' hH'H hJ'J
                (upper.extension.extensionQuotientMulEquiv.abelianizationCongr
                  z)))) := by
    simpa only [← abelianizationCongr_trans,
      ← abelianizationCongr_symm,
      MulEquiv.trans_apply,
      MulEquiv.symm_apply_apply] using
      AmbientEmbeddedFixedFieldPresentation.quotientRestriction
        K K' L L' lower upper hH'H hJ'J restrictActual hbase hcompat
        (upper.extension.extensionQuotientMulEquiv.abelianizationCongr z)
  have hambient :
      lower.extension.extensionQuotientMulEquiv.abelianizationCongr.symm
          (normResidueNaturalityAbelianizedRestriction
            H H' J J' hJH hJ'H' hH'H hJ'J
            (upper.extension.extensionQuotientMulEquiv.abelianizationCongr
              upperQuotientValue)) =
        lowerQuotientValue := by
    refine
      lower.extension.extensionQuotientMulEquiv.abelianizationCongr.symm_apply_eq.mpr ?_
    calc
      normResidueNaturalityAbelianizedRestriction
          H H' J J' hJH hJ'H' hH'H hJ'J
          (upper.extension.extensionQuotientMulEquiv.abelianizationCongr
            upperQuotientValue) =
          normResidueNaturalityAbelianizedRestriction
            H H' J J' hJH hJ'H' hH'H hJ'J
            ((upper.extension.extensionQuotientMulEquiv.symm.trans
              upper.fixedFieldQuotientEquiv).abelianizationCongr.symm
              upperSymbolValue) := by
        simp only [← abelianizationCongr_trans,
          ← abelianizationCongr_symm, MulEquiv.symm_trans_apply,
          MulEquiv.symm_symm, upperQuotientValue]
      _ = (lower.extension.extensionQuotientMulEquiv.symm.trans
            lower.fixedFieldQuotientEquiv).abelianizationCongr.symm
            lowerSymbolValue := hraw
      _ = lower.extension.extensionQuotientMulEquiv.abelianizationCongr
            lowerQuotientValue := by
        simp only [← abelianizationCongr_trans,
          ← abelianizationCongr_symm, MulEquiv.symm_trans_apply,
          MulEquiv.symm_symm, lowerQuotientValue]
  have hupperEval :
      upper.normResidueAbelianElement a =
        upper.quotientEquiv.abelianizationCongr
          upperQuotientValue := by
    exact upper.normResidueAbelianElement_apply a
  have hlowerEval :
      lower.normResidueAbelianElement aNorm =
        lower.quotientEquiv.abelianizationCongr
          lowerQuotientValue := by
    exact lower.normResidueAbelianElement_apply aNorm
  let ambientUpper : Gal(L' / K') :=
    ambientEmbeddedNormResidueElement K K' L' j eUpper a
  let ambientLower : Gal(L / K) :=
    ambientEmbeddedNormResidueElement K K L jLower eLower aNorm
  have htransport :
      restrictActual ambientUpper = ambientLower := by
    dsimp only [ambientUpper, ambientLower,
      ambientEmbeddedNormResidueElement,
      ambientEmbeddedNormResidueAbelianElement]
    change
      restrictActual
          ((Abelianization.equivOfComm (H := Gal(L' / K'))).symm
            (upper.normResidueAbelianElement a)) =
        (Abelianization.equivOfComm (H := Gal(L / K))).symm
          (lower.normResidueAbelianElement aNorm)
    rw [hupperEval, hlowerEval]
    calc
      restrictActual
          ((Abelianization.equivOfComm (H := Gal(L' / K'))).symm
            (upper.quotientEquiv.abelianizationCongr
              upperQuotientValue)) =
        (Abelianization.equivOfComm (H := Gal(L / K))).symm
            (lower.quotientEquiv.abelianizationCongr
              (lower.extension.extensionQuotientMulEquiv.abelianizationCongr.symm
                (normResidueNaturalityAbelianizedRestriction
                  H H' J J' hJH hJ'H' hH'H hJ'J
                  (upper.extension.extensionQuotientMulEquiv.abelianizationCongr
                    upperQuotientValue)))) :=
        htarget upperQuotientValue
      _ = (Abelianization.equivOfComm (H := Gal(L / K))).symm
            (lower.quotientEquiv.abelianizationCongr
              lowerQuotientValue) :=
        congrArg
          (fun z =>
            (Abelianization.equivOfComm (H := Gal(L / K))).symm
              (lower.quotientEquiv.abelianizationCongr z))
          hambient
  change
    restrictActual ambientUpper = ambientLower
  exact htransport
theorem

abelianLocalArtinMonoidHom_norm_restriction

L686 ↗
LocalClassFieldTheory.abelianLocalArtinMonoidHom_norm_restriction
Documentation

The actual finite abelian local Artin maps satisfy norm--restriction naturality in an arbitrary finite square of nonarchimedean local fields.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped IsMulCommutative ValuativeRel
Lean source · statement
theorem abelianLocalArtinMonoidHom_norm_restriction
    (K K' L L' : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field K'] [ValuativeRel K'] [TopologicalSpace K']
    [IsNonarchimedeanLocalField K']
    [Field L] [Field L']
    [Algebra K K'] [Algebra K L] [Algebra K L']
    [Algebra K' L'] [Algebra L L']
    [IsScalarTower K K' L'] [IsScalarTower K L L']
    [FiniteDimensional K K'] [Algebra.IsSeparable K K']
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation K')]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [FiniteDimensional K' L'] [IsAbelianGalois K' L'] :
    ((AlgEquiv.restrictNormalHom L).comp
        (AlgEquiv.restrictScalarsHom K)).comp
        (abelianLocalArtinMonoidHom K' L') =
      (abelianLocalArtinMonoidHom K L).comp
        (normUnits K K')

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.