CrossLocalRestriction.lean

theorem finitePlaceArtinLocalizedCompletion_algebraMap
    {F M : Type}
    [Field F] [NumberField F]
    [Field M] [NumberField M]
    [Algebra F M] [FiniteDimensional F M]
    (v : HeightOneSpectrum (𝓞 F))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv F v) M)
    (x : (NumberField.HeightOneSpectrum.adicAbv F v).Completion) :
    let vF := NumberField.HeightOneSpectrum.adicAbv F v
    let hvF : vF.IsNontrivial :=
      RayClass.adicAbv_isNontrivial v
    letI hMF :=
      AbsoluteValue.extensionCompletionAlgebra
        (K := F) w.1
    letI : SMul F w.1.Completion := hMF.toSMul
    letI : Algebra vF.Completion w.1.Completion :=
      AbsoluteValue.completionAlgebra vF w.1 w.2
    let E := AlgebraicNumberTheory.Valuations.LocalizedCompletion vF w
    let U := finitePlaceExtensionEquivAbove
      (K := F) (L := M) v w
    let eF :
        vF.Completion ≃+* v.adicCompletion F :=
      (relativeFinitePlaceCompletionAlgEquiv v).toRingEquiv
    let eE :
        E ≃+* U.1.adicCompletion M :=
      (AlgebraicNumberTheory.Valuations.localizedCompletionEquivCompletion
          vF hvF w).toRingEquiv.trans
        (finitePlaceExtensionAdicCompletionRingEquiv
          (K := F) (L := M) v w)
    eE (algebraMap vF.Completion E x) =
      finitePlaceAdicCompletionMap
        F M v U (eF x) := by
  let vF := NumberField.HeightOneSpectrum.adicAbv F v
  let hvF : vF.IsNontrivial :=
    RayClass.adicAbv_isNontrivial v
  let hMF :=
    AbsoluteValue.extensionCompletionAlgebra
      (K := F) w.1
  let : SMul F w.1.Completion := hMF.toSMul
  let : Algebra vF.Completion w.1.Completion :=
    AbsoluteValue.completionAlgebra vF w.1 w.2
  let E := AlgebraicNumberTheory.Valuations.LocalizedCompletion vF w
  let U := finitePlaceExtensionEquivAbove
    (K := F) (L := M) v w
  let eF :
      vF.Completion ≃+* v.adicCompletion F :=
    (relativeFinitePlaceCompletionAlgEquiv v).toRingEquiv
  let eE :
      E ≃+* U.1.adicCompletion M :=
    (AlgebraicNumberTheory.Valuations.localizedCompletionEquivCompletion
        vF hvF w).toRingEquiv.trans
      (finitePlaceExtensionAdicCompletionRingEquiv
        (K := F) (L := M) v w)
  change
    finitePlaceExtensionAdicCompletionRingEquiv
        (K := F) (L := M) v w
        (AlgebraicNumberTheory.Valuations.localizedCompletionEquivCompletion
          vF hvF w (algebraMap vF.Completion E x)) =
      finitePlaceAdicCompletionMap
        F M v U
          (relativeFinitePlaceCompletionAlgEquiv v x)
  rw [
    (AlgebraicNumberTheory.Valuations.localizedCompletionEquivCompletion
      vF hvF w).commutes]
  rw [←
    finitePlaceExtensionAdicCompletionMap_eq_finitePlaceAdicCompletionMap
      F M v w]
  change
    finitePlaceExtensionAdicCompletionRingEquiv
        (K := F) (L := M) v w
        (algebraMap vF.Completion w.1.Completion x) =
      finitePlaceExtensionAdicCompletionRingEquiv
        (K := F) (L := M) v w
        (AbsoluteValue.completionMap vF w.1 w.2
          ((relativeFinitePlaceCompletionAlgEquiv v).symm
            (relativeFinitePlaceCompletionAlgEquiv v x)))
  rw [
    (relativeFinitePlaceCompletionAlgEquiv v).symm_apply_apply,
    AbsoluteValue.completionAlgebra_algebraMap]

def finitePlaceArtinRelativeCompletionRingHom
    {K' : Type} [Field K'] [NumberField K']
    [Algebra K K']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (hW : finitePlaceBelow (K := K) W = v) :
    (NumberField.HeightOneSpectrum.adicAbv K v).Completion →+*
      (NumberField.HeightOneSpectrum.adicAbv K' W).Completion

theorem finitePlaceArtinRelativeCompletionRingHom_continuous
    {K' : Type} [Field K'] [NumberField K']
    [Algebra K K']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (hW : finitePlaceBelow (K := K) W = v) :
    Continuous
      (finitePlaceArtinRelativeCompletionRingHom
        (K := K) (K' := K') v W hW)

abbrev finitePlaceArtinLocalizedCompletion
    (F M : Type) [Field F] [NumberField F]
    [Field M] [NumberField M] [Algebra F M]
    (v : HeightOneSpectrum (𝓞 F))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv F v) M) : Type

def finitePlaceArtinLocalizedCompletionBaseRingHom
    (F M : Type) [Field F] [NumberField F]
    [Field M] [NumberField M] [Algebra F M]
    (v : HeightOneSpectrum (𝓞 F))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv F v) M) :
    (NumberField.HeightOneSpectrum.adicAbv F v).Completion →+*
      finitePlaceArtinLocalizedCompletion F M v w

def finitePlaceArtinLocalizedCompletionRingHom
    {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [NumberField L]
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
    (hcentres :
      finitePlaceBelow (K := L)
          (finitePlaceExtensionCentre
            (K := K') (L := L') W w') =
        finitePlaceExtensionCentre
          (K := K) (L := L) v w) :
    finitePlaceArtinLocalizedCompletion K L v w →+*
      finitePlaceArtinLocalizedCompletion K' L' W w'

theorem finitePlaceArtinLocalizedCompletion_towerPoint
    {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [NumberField L]
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (hW : finitePlaceBelow (K := K) W = v)
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
    (hcentres :
      finitePlaceBelow (K := L)
          (finitePlaceExtensionCentre
            (K := K') (L := L') W w') =
        finitePlaceExtensionCentre
          (K := K) (L := L) v w)
    (x : (NumberField.HeightOneSpectrum.adicAbv K v).Completion) :
    finitePlaceArtinLocalizedCompletionBaseRingHom K' L' W w'
        (finitePlaceArtinRelativeCompletionRingHom
          (K := K) (K' := K') v W hW x) =
      finitePlaceArtinLocalizedCompletionRingHom
        (K := K) (L := L) (K' := K') (L' := L')
        v W w w' hcentres
        (finitePlaceArtinLocalizedCompletionBaseRingHom K L v w x)

theorem finitePlaceArtinLocalizedCompletion_globalEmbedding
    {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [NumberField L]
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
    (hcentres :
      finitePlaceBelow (K := L)
          (finitePlaceExtensionCentre
            (K := K') (L := L') W w') =
        finitePlaceExtensionCentre
          (K := K) (L := L) v w)
    (x : L) :
    let vK := NumberField.HeightOneSpectrum.adicAbv K v
    let vK' := NumberField.HeightOneSpectrum.adicAbv K' W
    letI hwK :=
      AbsoluteValue.extensionCompletionAlgebra
        (K := K) w.1
    letI : SMul K w.1.Completion := hwK.toSMul
    letI : Algebra vK.Completion w.1.Completion :=
      AbsoluteValue.completionAlgebra vK w.1 w.2
    letI hwK' :=
      AbsoluteValue.extensionCompletionAlgebra
        (K := K') w'.1
    letI : SMul K' w'.1.Completion := hwK'.toSMul
    letI : Algebra vK'.Completion w'.1.Completion :=
      AbsoluteValue.completionAlgebra vK' w'.1 w'.2
    let E := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK w
    let E' := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK' w'
    letI : Algebra E E' :=
      (finitePlaceArtinLocalizedCompletionRingHom
        (K := K) (L := L) (K' := K') (L' := L')
        v W w w' hcentres).toAlgebra
    algebraMap E E'
        (AbsoluteValue.toAlgebraicLocalization
          vK w.1 w.2 x) =
      AbsoluteValue.toAlgebraicLocalization
        vK' w'.1 w'.2 (algebraMap L L' x) := by
  let vK := NumberField.HeightOneSpectrum.adicAbv K v
  let vK' := NumberField.HeightOneSpectrum.adicAbv K' W
  let hvK : vK.IsNontrivial :=
    RayClass.adicAbv_isNontrivial v
  let hvK' : vK'.IsNontrivial :=
    RayClass.adicAbv_isNontrivial W
  let hwK :=
    AbsoluteValue.extensionCompletionAlgebra
      (K := K) w.1
  let : SMul K w.1.Completion := hwK.toSMul
  let : Algebra vK.Completion w.1.Completion :=
    AbsoluteValue.completionAlgebra vK w.1 w.2
  let hwK' :=
    AbsoluteValue.extensionCompletionAlgebra
      (K := K') w'.1
  let : SMul K' w'.1.Completion := hwK'.toSMul
  let : Algebra vK'.Completion w'.1.Completion :=
    AbsoluteValue.completionAlgebra vK' w'.1 w'.2
  let E := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK w
  let E' := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK' w'
  let : Algebra E E' :=
    (finitePlaceArtinLocalizedCompletionRingHom
      (K := K) (L := L) (K' := K') (L' := L')
      v W w w' hcentres).toAlgebra
  let U :=
    finitePlaceExtensionEquivAbove
      (K := K) (L := L) v w
  let U' :=
    finitePlaceExtensionEquivAbove
      (K := K') (L := L') W w'
  have hU'L : finitePlaceBelow (K := L) U'.1 = U.1 := by
    simpa only [
      U, U',
      finitePlaceExtensionEquivAbove_coe
    ] using hcentres
  let eE :
      E ≃+* U.1.adicCompletion L :=
    (AlgebraicNumberTheory.Valuations.localizedCompletionEquivCompletion
        vK hvK w).toRingEquiv.trans
      (finitePlaceExtensionAdicCompletionRingEquiv
        (K := K) (L := L) v w)
  let eE' :
      E' ≃+* U'.1.adicCompletion L' :=
    (AlgebraicNumberTheory.Valuations.localizedCompletionEquivCompletion
        vK' hvK' w').toRingEquiv.trans
      (finitePlaceExtensionAdicCompletionRingEquiv
        (K := K') (L := L') W w')
  have hLowerConcrete :
      eE
          (AbsoluteValue.toAlgebraicLocalization
            vK w.1 w.2 x) =
        FinitePlace.embedding U.1 x := by
    change
      finitePlaceExtensionAdicCompletionRingEquiv
          (K := K) (L := L) v w
          (AlgebraicNumberTheory.Valuations.localizedCompletionEquivCompletion
            vK hvK w
            (AbsoluteValue.toAlgebraicLocalization
              vK w.1 w.2 x)) =
        FinitePlace.embedding U.1 x
    rw [
      AlgebraicNumberTheory.Valuations.localizedCompletionEquivCompletion_coe]
    change
      finitePlaceExtensionAdicCompletionRingEquiv
          (K := K) (L := L) v w
          (AbsoluteValue.toCompletion w.1 x) =
        FinitePlace.embedding
          (finitePlaceExtensionCentre
            (K := K) (L := L) v w) x
    exact
      finitePlaceExtensionAdicCompletionRingEquiv_toCompletion
        (K := K) (L := L) v w x
  have hUpperConcrete :
      eE'
          (AbsoluteValue.toAlgebraicLocalization
            vK' w'.1 w'.2 (algebraMap L L' x)) =
        FinitePlace.embedding U'.1 (algebraMap L L' x) := by
    change
      finitePlaceExtensionAdicCompletionRingEquiv
          (K := K') (L := L') W w'
          (AlgebraicNumberTheory.Valuations.localizedCompletionEquivCompletion
            vK' hvK' w'
            (AbsoluteValue.toAlgebraicLocalization
              vK' w'.1 w'.2 (algebraMap L L' x))) =
        FinitePlace.embedding U'.1 (algebraMap L L' x)
    rw [
      AlgebraicNumberTheory.Valuations.localizedCompletionEquivCompletion_coe]
    change
      finitePlaceExtensionAdicCompletionRingEquiv
          (K := K') (L := L') W w'
          (AbsoluteValue.toCompletion w'.1 (algebraMap L L' x)) =
        FinitePlace.embedding
          (finitePlaceExtensionCentre
            (K := K') (L := L') W w')
          (algebraMap L L' x)
    exact
      finitePlaceExtensionAdicCompletionRingEquiv_toCompletion
        (K := K') (L := L') W w' (algebraMap L L' x)
  apply eE'.injective
  change
    eE'
        (eE'.symm
          (finitePlaceAdicCompletionMap
            L L' U.1 ⟨U'.1, hU'L⟩
            (eE
              (AbsoluteValue.toAlgebraicLocalization
                vK w.1 w.2 x)))) =
      eE'
        (AbsoluteValue.toAlgebraicLocalization
          vK' w'.1 w'.2 (algebraMap L L' x))
  rw [eE'.apply_symm_apply, hLowerConcrete, hUpperConcrete]
  change
    finitePlaceAdicCompletionMap
        L L' U.1 ⟨U'.1, hU'L⟩
        (x : U.1.adicCompletion L) =
      (algebraMap L L' x : U'.1.adicCompletion L')
  exact
    finitePlaceAdicCompletionMap_coe
      L L' U.1 ⟨U'.1, hU'L⟩ x

abbrev finitePlaceArtinLocalizedAutomorphism
    (F M : Type) [Field F] [NumberField F]
    [Field M] [NumberField M] [Algebra F M]
    (v : HeightOneSpectrum (𝓞 F))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv F v) M) : Type

def finitePlaceCrossLocalRestrictionMonoidHom
    {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [NumberField L]
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (hW : finitePlaceBelow (K := K) W = v)
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
    (hcentres :
      finitePlaceBelow (K := L)
          (finitePlaceExtensionCentre
            (K := K') (L := L') W w') =
        finitePlaceExtensionCentre
          (K := K) (L := L) v w) :
    finitePlaceArtinLocalizedAutomorphism K' L' W w' →*
      finitePlaceArtinLocalizedAutomorphism K L v w

theorem finitePlaceDecompositionEquiv_symm_action
    {F M : Type}
    [Field F] [Field M] [Algebra F M] [IsGalois F M]
    (vF : AbsoluteValue F ℝ)
    (hvF : vF.IsNontrivial)
    (wF : AbsoluteValueExtension vF M)
    (tau :
      letI hwF :=
        AbsoluteValue.extensionCompletionAlgebra
          (K := F) wF.1
      letI : SMul F wF.1.Completion := hwF.toSMul
      letI : Algebra vF.Completion wF.1.Completion :=
        AbsoluteValue.completionAlgebra vF wF.1 wF.2
      let E :=
        AlgebraicNumberTheory.Valuations.LocalizedCompletion vF wF
      E ≃ₐ[vF.Completion] E)
    (z : M) :
    letI hwF :=
      AbsoluteValue.extensionCompletionAlgebra
        (K := F) wF.1
    letI : SMul F wF.1.Completion := hwF.toSMul
    letI : Algebra vF.Completion wF.1.Completion :=
      AbsoluteValue.completionAlgebra vF wF.1 wF.2
    let E :=
      AlgebraicNumberTheory.Valuations.LocalizedCompletion vF wF
    let e :
        absoluteValueDecompositionGroup F wF.1 ≃*
          (E ≃ₐ[vF.Completion] E) :=
      decompositionGroupEquivAlgebraicLocalizationAut
        vF hvF wF
    let embedding : M →+* E :=
      AbsoluteValue.toAlgebraicLocalization vF wF.1 wF.2
    embedding (((e.symm tau).1 : M ≃ₐ[F] M) z) =
      tau (embedding z) := by
  let hwF :=
    AbsoluteValue.extensionCompletionAlgebra
      (K := F) wF.1
  let : SMul F wF.1.Completion := hwF.toSMul
  let : Algebra vF.Completion wF.1.Completion :=
    AbsoluteValue.completionAlgebra vF wF.1 wF.2
  let E :=
    AlgebraicNumberTheory.Valuations.LocalizedCompletion vF wF
  let e :
      absoluteValueDecompositionGroup F wF.1 ≃*
        (E ≃ₐ[vF.Completion] E) :=
    decompositionGroupEquivAlgebraicLocalizationAut
      vF hvF wF
  let embedding : M →+* E :=
    AbsoluteValue.toAlgebraicLocalization vF wF.1 wF.2
  calc
    embedding (((e.symm tau).1 : M ≃ₐ[F] M) z) =
        e (e.symm tau) (embedding z) := by
      rw [
        localizationRamificationGroups_decompositionGroupEquiv_toLocalization]
    _ = tau (embedding z) := by
      rw [e.apply_symm_apply]

theorem finitePlaceCrossDecompositionTransport_core
    {K K' L L' C D E E' : Type}
    [Field K] [Field K'] [Field L] [Field L']
    [Field C] [Field D] [Field E] [Field E']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra K L] [Algebra L L'] [IsScalarTower K L L']
    [Normal K L]
    [Algebra C D] [Algebra D E'] [Algebra C E']
    [IsScalarTower C D E']
    [Algebra C E] [Algebra E E'] [IsScalarTower C E E']
    [Normal C E]
    (phiLower : (E ≃ₐ[C] E) → (L ≃ₐ[K] L))
    (phiUpper : (E' ≃ₐ[D] E') → (L' ≃ₐ[K'] L'))
    (lowerEmbedding : L →+* E)
    (upperEmbedding : L' →+* E')
    (hEmbedding : ∀ z : L,
      algebraMap E E' (lowerEmbedding z) =
        upperEmbedding (algebraMap L L' z))
    (hUpperAction : ∀ (tau : E' ≃ₐ[D] E') (z : L'),
      upperEmbedding (phiUpper tau z) =
        tau (upperEmbedding z))
    (hLowerAction : ∀ (tau : E ≃ₐ[C] E) (z : L),
      tau (lowerEmbedding z) =
        lowerEmbedding (phiLower tau z))
    (tauUpper : E' ≃ₐ[D] E') :
    AlgEquiv.restrictNormalHom L
        (AlgEquiv.restrictScalarsHom K (phiUpper tauUpper)) =
      phiLower
        (AlgEquiv.restrictNormalHom E
          (AlgEquiv.restrictScalarsHom C tauUpper))

theorem finitePlaceCrossDecompositionTransport
    {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [NumberField L]
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (hW : finitePlaceBelow (K := K) W = v)
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
    (hcentres :
      finitePlaceBelow (K := L)
          (finitePlaceExtensionCentre
            (K := K') (L := L') W w') =
        finitePlaceExtensionCentre
          (K := K) (L := L) v w)
    (tauUpper : finitePlaceArtinLocalizedAutomorphism K' L' W w') :
    ((AlgEquiv.restrictNormalHom L).comp
        (AlgEquiv.restrictScalarsHom K))
        (finitePlaceLocalToGlobalMonoidHom
          (K := K') (L := L') W w' tauUpper) =
      finitePlaceLocalToGlobalMonoidHom
        (K := K) (L := L) v w
        (finitePlaceCrossLocalRestrictionMonoidHom
          (K := K) (L := L) (K' := K') (L' := L')
          v W hW w w' hcentres tauUpper)