MixedCharCyclotomicLogAction.lean

theorem characterLog_action_sub_prime_divisible_of_log_difference
    {M Γ : Type*} [Field M] [CharZero M] [Group Γ]
    (vE : _root_.Valuation M (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete vE]
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField vE.valuationSubring) p]
    (σ : Γ →* (M ≃+* M)) (hval : ∀ (g : Γ) (b : M), vE (σ g b) = vE b)
    (χ : Γ →* ℤ_[p]ˣ) (Δ : Subgroup Γ) [Δ.Normal]
    (g : Γ) (x : CharacterLogSpaceOfMixedChar vE p σ hval χ Δ)
    (z : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation vE) 1)
    (hz : σ g (characterLogInclusionOfMixedChar vE p σ hval χ Δ x) -
      padicIntToFieldOfMixedChar vE p (χ g : ℤ_[p]) *
        characterLogInclusionOfMixedChar vE p σ hval χ Δ x =
      (p : M) * (principalUnitLogOfMixedChar vE p z).toAdd) :
    ∃ y : CharacterLogSpaceOfMixedChar vE p σ hval χ Δ,
      characterLogRepresentationOfMixedChar vE p σ hval χ Δ g x - x =
        (p : ℤ_[p]) • y

theorem exists_cyclotomic_eigenunit_of_characterLog
    {F K E : Type*} [Field F] [Field K] [Field E]
    [Algebra F K] [Algebra K E] [Algebra F E] [IsScalarTower F K E]
    [CharZero E] [Normal F K]
    (vE : _root_.Valuation E (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete vE]
    (p : ℕ) [Fact p.Prime] [IsCyclotomicExtension {p} K E]
    [CharP (IsLocalRing.ResidueField vE.valuationSubring) p]
    (hval : ∀ (g : Gal(E/F)) (b : E),
      vE (MulSemiringAction.toRingEquiv Gal(E/F) E g b) = vE b)
    (x : CharacterLogSpaceOfMixedChar vE p
      (MulSemiringAction.toRingEquiv Gal(E/F) E) hval
      (primitiveRootTeichmullerCharacter F p (IsCyclotomicExtension.zeta_spec p K E))
      (AlgEquiv.restrictNormalHom K : Gal(E/F) →* Gal(K/F)).ker) :
    ∃ u : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation vE) 1,
      (principalUnitLogOfMixedChar vE p u).toAdd =
        characterLogInclusionOfMixedChar vE p
          (MulSemiringAction.toRingEquiv Gal(E/F) E) hval
          (primitiveRootTeichmullerCharacter F p (IsCyclotomicExtension.zeta_spec p K E))
          (AlgEquiv.restrictNormalHom K : Gal(E/F) →* Gal(K/F)).ker x ∧
      ∀ δ : Gal(E/K),
        δ (((u : (completeDVFOfWithZeroValuation vE).valuationSubringˣ) :
          (completeDVFOfWithZeroValuation vE).valuationSubring) : E) =
        (((principalUnitPadicPowOfMixedChar vE p
          (primeCyclotomicTeichmullerCharacter K E p δ : ℤ_[p]) u :
            (completeDVFOfWithZeroValuation vE).valuationSubringˣ) :
              (completeDVFOfWithZeroValuation vE).valuationSubring) : E)

theorem characterLog_action_sub_prime_divisible_of_trivial_lowerH1Action
    {F K Ω : Type*} [Field F] [Field K] [Field Ω]
    [Algebra F K] [Algebra K Ω] [IsAlgClosure K Ω] [CharZero K] [Normal F K]
    (E : IntermediateField K Ω) [Algebra F E] [IsScalarTower F K E]
    (vE : _root_.Valuation E (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete vE]
    (p : ℕ) [Fact p.Prime] [IsCyclotomicExtension {p} K E]
    [CharP (IsLocalRing.ResidueField vE.valuationSubring) p]
    (hval : ∀ (g : Gal(E/F)) (b : E),
      vE (MulSemiringAction.toRingEquiv Gal(E/F) E g b) = vE b)
    (htriv : ∀ τ : Gal(K/F), relativeGaloisH1Action (n := p) F K τ = 1) :
    let σ := MulSemiringAction.toRingEquiv Gal(E/F) E
    let χ := primitiveRootTeichmullerCharacter F p (IsCyclotomicExtension.zeta_spec p K E)
    let Δ := (AlgEquiv.restrictNormalHom K : Gal(E/F) →* Gal(K/F)).ker
    ∀ (g : Gal(E/F)) (x : CharacterLogSpaceOfMixedChar vE p σ hval χ Δ),
      ∃ y : CharacterLogSpaceOfMixedChar vE p σ hval χ Δ,
        characterLogRepresentationOfMixedChar vE p σ hval χ Δ g x - x =
          (p : ℤ_[p]) • y := by
  classical
  intro σ χ Δ g x
  obtain ⟨u, hulog, hueigen⟩ :=
    exists_cyclotomic_eigenunit_of_characterLog (F := F) (K := K) vE p hval x
  let τ := (AlgEquiv.restrictNormalHom K : Gal(E/F) →* Gal(K/F)) g
  have hcompat (b : K) : g (algebraMap K E b) = algebraMap K E (τ b) :=
    (g.restrictNormal_commutes K b).symm
  obtain ⟨z, hz⟩ := exists_principalUnit_log_character_difference_of_trivial_lowerH1Action
    E vE p (IsCyclotomicExtension.zeta_spec p K E) u hueigen τ g hcompat (hval g) (htriv τ)
  rw [hulog] at hz
  exact characterLog_action_sub_prime_divisible_of_log_difference
    vE p σ hval χ Δ g x z hz