AbsoluteMuPKummerLinear.lean

theorem absoluteMuP_orbit_isLocallyConstant (x : AbsoluteMuP K p) :
    IsLocallyConstant
      (fun sigma : Field.absoluteGaloisGroup K ↦
        absoluteMuPActionContinuousLinearMap K p sigma x) := by
  rw [IsLocallyConstant.iff_exists_open]
  intro sigma
  let alpha : AlgebraicClosure K := x.toMul.1
  let E := FiniteGaloisIntermediateField.adjoin K {alpha}
  let e := absoluteGaloisGroupContinuousMulEquiv K
  let H : Set Gal(AlgebraicClosure K/K) := E.fixingSubgroup
  refine ⟨e ⁻¹' (e sigma • H), ?_, ?_, ?_⟩
  · exact ((IntermediateField.fixingSubgroup_isOpen E.toIntermediateField).leftCoset
      (e sigma)).preimage e.continuous
  · change e sigma ∈ e sigma • H
    exact ⟨1, E.fixingSubgroup.one_mem, mul_one (e sigma)⟩
  · intro tau htau
    change e tau ∈ e sigma • H at htau
    rcases htau with ⟨h, hh, htau⟩
    have hfix : h alpha = alpha :=
      ((IntermediateField.mem_fixingSubgroup_iff E.toIntermediateField h).mp hh)
        alpha
        (FiniteGaloisIntermediateField.subset_adjoin K {alpha}
          (Set.mem_singleton alpha))
    have hfixUnit : h • x.toMul.1 = x.toMul.1 := by
      apply Units.ext
      exact hfix
    apply Additive.toMul.injective
    apply Subtype.ext
    change e tau • x.toMul.1 = e sigma • x.toMul.1
    change e sigma * h = e tau at htau
    rw [← htau, mul_smul, hfixUnit]

def absoluteMuPHomogeneousZeroCochain (x : AbsoluteMuP K p) :
    (TopRep.homogeneousCochains (absoluteMuPTopRep K p)).X 0

theorem absoluteMuPHomogeneousZeroCochain_boundary_apply
    (x : AbsoluteMuP K p)
    (g h : Field.absoluteGaloisGroup K) :
    (((TopRep.homogeneousCochains (absoluteMuPTopRep K p)).d 0 1).hom
        (absoluteMuPHomogeneousZeroCochain K p x)).1 g h =
      absoluteMuPActionContinuousLinearMap K p h x -
        absoluteMuPActionContinuousLinearMap K p g x

def absoluteKummerMuPMulCorrection (a b : Kˣ) : AbsoluteMuP K p

theorem absoluteKummerMuPMulCorrection_apply_coe (a b : Kˣ) :
    (absoluteKummerMuPMulCorrection K p a b).toMul.1 =
      absoluteKummerChosenRoot K p (a * b) /
        (absoluteKummerChosenRoot K p a * absoluteKummerChosenRoot K p b)

theorem absoluteKummerMuPRootCocycle_mul_sub
    (a b : Kˣ) (sigma : Field.absoluteGaloisGroup K) :
    absoluteKummerMuPRootCocycle K p (a * b) sigma -
          absoluteKummerMuPRootCocycle K p a sigma -
        absoluteKummerMuPRootCocycle K p b sigma =
      absoluteMuPActionContinuousLinearMap K p sigma
          (absoluteKummerMuPMulCorrection K p a b) -
        absoluteKummerMuPMulCorrection K p a b

theorem absoluteKummerMuPHomogeneousOneCochain_mul_sub_boundary
    (a b : Kˣ) :
    absoluteKummerMuPHomogeneousOneCochain K p (a * b) -
          (absoluteKummerMuPHomogeneousOneCochain K p a +
            absoluteKummerMuPHomogeneousOneCochain K p b) =
      ((TopRep.homogeneousCochains (absoluteMuPTopRep K p)).d 0 1).hom
        (absoluteMuPHomogeneousZeroCochain K p
          (absoluteKummerMuPMulCorrection K p a b))

theorem absoluteKummerMuPHomogeneousOneCocycle_mul_sub_boundary
    (a b : Kˣ) :
    absoluteKummerMuPHomogeneousOneCocycle K p (a * b) -
          (absoluteKummerMuPHomogeneousOneCocycle K p a +
            absoluteKummerMuPHomogeneousOneCocycle K p b) =
      ((TopRep.homogeneousCochains (absoluteMuPTopRep K p)).toCycles 0 1).hom
        (absoluteMuPHomogeneousZeroCochain K p
          (absoluteKummerMuPMulCorrection K p a b))

theorem absoluteKummerMuPH1Class_mul (a b : Kˣ) :
    absoluteKummerMuPH1Class K p (a * b) =
      absoluteKummerMuPH1Class K p a +
        absoluteKummerMuPH1Class K p b

def absoluteKummerMuPH1LinearMap :
    absolutePowerClassModP K p →ₗ[ZMod p]
      continuousCohomology 1 (absoluteMuPTopRep K p)

theorem absoluteKummerMuPH1LinearMap_mk (a : Kˣ) :
    absoluteKummerMuPH1LinearMap K p
        (Additive.ofMul
          (QuotientGroup.mk'
            (powMonoidHom p : Kˣ →* Kˣ).range a)) =
      absoluteKummerMuPH1Class K p a