NormalBasis.lean

theorem span_normalBasis_eq_chosenNormalBasisIntegerLattice :
    Submodule.span 𝒪[K] (Set.range (IsGalois.normalBasis K L)) =
      chosenNormalBasisIntegerLattice K L

def chosenNormalBasisIntegerLatticeBasis :
    Module.Basis Gal(L / K) 𝒪[K] (chosenNormalBasisIntegerLattice K L)

theorem chosenNormalBasisIntegerLatticeBasis_apply (σ : Gal(L/K)) :
    ((chosenNormalBasisIntegerLatticeBasis K L σ :
      chosenNormalBasisIntegerLattice K L) : L) = IsGalois.normalBasis K L σ

def chosenNormalBasisIntegerLatticeMulPowLinearMap (n : Nat) :
    chosenNormalBasisIntegerLattice K L →ₗ[𝒪[K]]
      chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) where
  toFun x :=
    ⟨algebraMap 𝒪[K] L (chosenIntegerRingUniformizer K ^ n) * (x : L),
      (mem_chosenBaseUniformizerPowSubmodule_iff
        (K := K) (L := L) n (chosenNormalBasisIntegerLattice K L) _).2
        ⟨x, x.2, rfl⟩⟩
  map_add' := by
    intro x y
    ext
    exact mul_add _ _ _
  map_smul' := by
    intro a x
    ext
    simp [Algebra.smul_def, mul_assoc, mul_comm, mul_left_comm]

theorem chosenNormalBasisIntegerLatticeMulPowLinearMap_bijective (n : Nat) :
    Function.Bijective (chosenNormalBasisIntegerLatticeMulPowLinearMap K L n)

def chosenNormalBasisIntegerLatticeMulPowLinearEquiv (n : Nat) :
    chosenNormalBasisIntegerLattice K L ≃ₗ[𝒪[K]]
      chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L)

theorem chosenNormalBasisIntegerLatticeMulPowLinearEquiv_apply
    (n : Nat) (x : chosenNormalBasisIntegerLattice K L) :
    ((chosenNormalBasisIntegerLatticeMulPowLinearEquiv K L n x :
      chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L)) : L) =
      algebraMap 𝒪[K] L (chosenIntegerRingUniformizer K ^ n) * (x : L)

def chosenNormalBasisIntegerLatticeUniformizerSubmodule :
    Submodule 𝒪[K] (chosenNormalBasisIntegerLattice K L)

theorem mem_chosenNormalBasisIntegerLatticeUniformizerSubmodule_iff
    (x : chosenNormalBasisIntegerLattice K L) :
    x ∈ chosenNormalBasisIntegerLatticeUniformizerSubmodule K L ↔
      (x : L) ∈ chosenBaseUniformizerPowSubmodule K L 1
        (chosenNormalBasisIntegerLattice K L)

theorem chosenNormalBasisIntegerLatticeUniformizerSubmodule_map_mulPow
    (n : Nat) :
    (chosenNormalBasisIntegerLatticeUniformizerSubmodule K L).map
        (chosenNormalBasisIntegerLatticeMulPowLinearEquiv K L n :
          chosenNormalBasisIntegerLattice K L →ₗ[𝒪[K]]
            chosenBaseUniformizerPowSubmodule K L n
              (chosenNormalBasisIntegerLattice K L)) =
      chosenNormalBasisLatticeSuccSubmodule K L n

def chosenNormalBasisLatticeSuccQuotToIntegerLatticeQuotLinearEquiv
    (n : Nat) :
    chosenNormalBasisLatticeSuccQuot K L n ≃ₗ[𝒪[K]]
      (chosenNormalBasisIntegerLattice K L ⧸
        chosenNormalBasisIntegerLatticeUniformizerSubmodule K L)

theorem chosenNormalBasisLatticeSuccQuotToIntegerLatticeQuotLinearEquiv_mk_mulPow
    (n : Nat) (x : chosenNormalBasisIntegerLattice K L) :
    chosenNormalBasisLatticeSuccQuotToIntegerLatticeQuotLinearEquiv K L n
        (chosenNormalBasisLatticeSuccQuotMk K L n
          (chosenNormalBasisIntegerLatticeMulPowLinearEquiv K L n x)) =
      Submodule.Quotient.mk x

def chosenNormalBasisCoordinateMaximalSubmodule :
    Submodule 𝒪[K] (Gal(L / K) → 𝒪[K])

theorem mem_chosenNormalBasisCoordinateMaximalSubmodule_iff
    (f : Gal(L/K) → 𝒪[K]) :
    f ∈ chosenNormalBasisCoordinateMaximalSubmodule K L ↔
      ∀ σ : Gal(L / K), f σ ∈ (𝓂[K] : Ideal 𝒪[K])

theorem chosenNormalBasisIntegerLatticeUniformizerSubmodule_map_equivFun :
    (chosenNormalBasisIntegerLatticeUniformizerSubmodule K L).map
        ((chosenNormalBasisIntegerLatticeBasis K L).equivFun :
          chosenNormalBasisIntegerLattice K L →ₗ[𝒪[K]] (Gal(L / K) → 𝒪[K])) =
      chosenNormalBasisCoordinateMaximalSubmodule K L

def chosenNormalBasisIntegerLatticeQuotCoordinateQuotLinearEquiv :
    (chosenNormalBasisIntegerLattice K L ⧸
        chosenNormalBasisIntegerLatticeUniformizerSubmodule K L) ≃ₗ[𝒪[K]]
      ((Gal(L / K) → 𝒪[K]) ⧸ chosenNormalBasisCoordinateMaximalSubmodule K L)

def chosenNormalBasisCoordinateQuotPiLinearEquiv :
    ((Gal(L / K) → 𝒪[K]) ⧸ chosenNormalBasisCoordinateMaximalSubmodule K L) ≃ₗ[𝒪[K]]
      (Gal(L / K) → (𝒪[K] ⧸ (𝓂[K] : Ideal 𝒪[K])))

theorem chosenNormalBasisCoordinateQuotPiLinearEquiv_mk
    (f : Gal(L/K) → 𝒪[K]) :
    chosenNormalBasisCoordinateQuotPiLinearEquiv K L
        (Submodule.Quotient.mk f) =
      fun σ : Gal(L / K) => Submodule.Quotient.mk (f σ) :=
  rfl

def chosenNormalBasisPiResidueInverseIndexAddEquiv :
    (Gal(L / K) → (𝒪[K] ⧸ (𝓂[K] : Ideal 𝒪[K]))) ≃+
      (Gal(L / K) → 𝓀[K]) where
  toFun f σ := integerRingModMaximalIdealAddEquivResidue K (f σ⁻¹)
  invFun f σ := (integerRingModMaximalIdealAddEquivResidue K).symm (f σ⁻¹)
  left_inv := by
    intro f
    funext σ
    simp
  right_inv := by
    intro f
    funext σ
    simp
  map_add' := by
    intro f g
    funext σ
    simp

theorem chosenNormalBasisPiResidueInverseIndexAddEquiv_apply
    (f : Gal(L/K) → (𝒪[K] ⧸ (𝓂[K] : Ideal 𝒪[K])))
    (σ : Gal(L/K)) :
    chosenNormalBasisPiResidueInverseIndexAddEquiv K L f σ =
      integerRingModMaximalIdealAddEquivResidue K (f σ⁻¹)

def chosenNormalBasisLatticeSuccQuotRightRegularAddEquiv (n : Nat) :
    chosenNormalBasisLatticeSuccQuot K L n ≃+ (Gal(L / K) → 𝓀[K])

theorem chosenNormalBasisLatticeSuccQuotRightRegularAddEquiv_mk_mulPow
    (n : Nat) (x : chosenNormalBasisIntegerLattice K L) (σ : Gal(L/K)) :
    chosenNormalBasisLatticeSuccQuotRightRegularAddEquiv K L n
        (chosenNormalBasisLatticeSuccQuotMk K L n
          (chosenNormalBasisIntegerLatticeMulPowLinearEquiv K L n x)) σ =
      IsLocalRing.residue 𝒪[K]
        ((chosenNormalBasisIntegerLatticeBasis K L).equivFun x σ⁻¹)

def galoisGroupChosenNormalBasisIntegerLatticeLinearEquiv (τ : Gal(L/K)) :
    chosenNormalBasisIntegerLattice K L ≃ₗ[𝒪[K]]
      chosenNormalBasisIntegerLattice K L where
  toFun x := ⟨τ (x : L),
    galoisGroup_apply_mem_chosenNormalBasisIntegerLattice (K := K) (L := L) τ x.2⟩
  invFun x := ⟨τ⁻¹ (x : L),
    galoisGroup_apply_mem_chosenNormalBasisIntegerLattice (K := K) (L := L) τ⁻¹ x.2⟩
  left_inv x := by
    apply Subtype.ext
    exact τ.symm_apply_apply (x : L)
  right_inv x := by
    apply Subtype.ext
    exact τ.apply_symm_apply (x : L)
  map_add' x y := by
    apply Subtype.ext
    exact map_add τ (x : L) (y : L)
  map_smul' a x := by
    apply Subtype.ext
    have ha : τ (algebraMap 𝒪[K] L a) = algebraMap 𝒪[K] L a := by
      change τ (algebraMap K L (a : K)) = algebraMap K L (a : K)
      exact τ.commutes (a : K)
    change τ (((a • x : chosenNormalBasisIntegerLattice K L) : L)) =
      ((a • (⟨τ (x : L), galoisGroup_apply_mem_chosenNormalBasisIntegerLattice
        (K := K) (L := L) τ x.2⟩ : chosenNormalBasisIntegerLattice K L) :
          chosenNormalBasisIntegerLattice K L) : L)
    rw [Submodule.coe_smul, Submodule.coe_smul]
    rw [Algebra.smul_def, Algebra.smul_def]
    rw [map_mul, ha]

theorem galoisGroupChosenNormalBasisIntegerLatticeLinearEquiv_apply_coe
    (τ : Gal(L/K)) (x : chosenNormalBasisIntegerLattice K L) :
    ((galoisGroupChosenNormalBasisIntegerLatticeLinearEquiv K L τ x :
      chosenNormalBasisIntegerLattice K L) : L) = τ (x : L)

theorem galoisGroupChosenNormalBasisIntegerLatticeLinearEquiv_one_apply
    (x : chosenNormalBasisIntegerLattice K L) :
    galoisGroupChosenNormalBasisIntegerLatticeLinearEquiv K L 1 x = x

theorem galoisGroupChosenNormalBasisIntegerLatticeLinearEquiv_mul_apply
    (τ υ : Gal(L/K)) (x : chosenNormalBasisIntegerLattice K L) :
    galoisGroupChosenNormalBasisIntegerLatticeLinearEquiv K L (τ * υ) x =
      galoisGroupChosenNormalBasisIntegerLatticeLinearEquiv K L τ
        (galoisGroupChosenNormalBasisIntegerLatticeLinearEquiv K L υ x)

theorem chosenNormalBasisIntegerLatticeBasis_equivFun_galoisGroup
    (τ σ : Gal(L/K)) (x : chosenNormalBasisIntegerLattice K L) :
    (chosenNormalBasisIntegerLatticeBasis K L).equivFun
        (galoisGroupChosenNormalBasisIntegerLatticeLinearEquiv K L τ x) σ =
      (chosenNormalBasisIntegerLatticeBasis K L).equivFun x (τ⁻¹ * σ)

theorem chosenNormalBasisIntegerLatticeUniformizerSubmodule_map_galoisGroup
    (τ : Gal(L/K)) :
    (chosenNormalBasisIntegerLatticeUniformizerSubmodule K L).map
        (galoisGroupChosenNormalBasisIntegerLatticeLinearEquiv K L τ :
          chosenNormalBasisIntegerLattice K L →ₗ[𝒪[K]]
            chosenNormalBasisIntegerLattice K L) =
      chosenNormalBasisIntegerLatticeUniformizerSubmodule K L

def galoisGroupChosenNormalBasisIntegerLatticeQuotLinearEquiv
    (τ : Gal(L/K)) :
    (chosenNormalBasisIntegerLattice K L ⧸
        chosenNormalBasisIntegerLatticeUniformizerSubmodule K L) ≃ₗ[𝒪[K]]
      (chosenNormalBasisIntegerLattice K L ⧸
        chosenNormalBasisIntegerLatticeUniformizerSubmodule K L)

theorem galoisGroupChosenNormalBasisIntegerLatticeQuotLinearEquiv_mk
    (τ : Gal(L/K)) (x : chosenNormalBasisIntegerLattice K L) :
    galoisGroupChosenNormalBasisIntegerLatticeQuotLinearEquiv K L τ
        (Submodule.Quotient.mk x) =
      Submodule.Quotient.mk
        (galoisGroupChosenNormalBasisIntegerLatticeLinearEquiv K L τ x)

def galoisGroupChosenNormalBasisLatticeSuccQuotAddEquiv
    (n : Nat) (τ : Gal(L/K)) :
    chosenNormalBasisLatticeSuccQuot K L n ≃+
      chosenNormalBasisLatticeSuccQuot K L n

theorem galoisGroupChosenNormalBasisLatticeSuccQuotAddEquiv_mk_mulPow
    (n : Nat) (τ : Gal(L/K)) (x : chosenNormalBasisIntegerLattice K L) :
    galoisGroupChosenNormalBasisLatticeSuccQuotAddEquiv K L n τ
        (chosenNormalBasisLatticeSuccQuotMk K L n
          (chosenNormalBasisIntegerLatticeMulPowLinearEquiv K L n x)) =
      chosenNormalBasisLatticeSuccQuotMk K L n
        (chosenNormalBasisIntegerLatticeMulPowLinearEquiv K L n
          (galoisGroupChosenNormalBasisIntegerLatticeLinearEquiv K L τ x))

theorem chosenNormalBasisLatticeSuccQuotToIntegerLatticeQuotLinearEquiv_galoisGroup
    (n : Nat) (τ : Gal(L/K))
    (q : chosenNormalBasisLatticeSuccQuot K L n) :
    chosenNormalBasisLatticeSuccQuotToIntegerLatticeQuotLinearEquiv K L n
        (galoisGroupChosenNormalBasisLatticeSuccQuotAddEquiv K L n τ q) =
      galoisGroupChosenNormalBasisIntegerLatticeQuotLinearEquiv K L τ
        (chosenNormalBasisLatticeSuccQuotToIntegerLatticeQuotLinearEquiv K L n q)

theorem chosenNormalBasisIntegerLatticeMulPowLinearEquiv_galoisGroup_apply_coe
    (n : Nat) (τ : Gal(L/K)) (x : chosenNormalBasisIntegerLattice K L) :
    ((chosenNormalBasisIntegerLatticeMulPowLinearEquiv K L n
      (galoisGroupChosenNormalBasisIntegerLatticeLinearEquiv K L τ x) :
        chosenBaseUniformizerPowSubmodule K L n
          (chosenNormalBasisIntegerLattice K L)) : L) =
      τ ((chosenNormalBasisIntegerLatticeMulPowLinearEquiv K L n x :
        chosenBaseUniformizerPowSubmodule K L n
          (chosenNormalBasisIntegerLattice K L)) : L)

def galoisGroupChosenNormalBasisLatticeSuccQuotDistribMulAction
    (n : Nat) :
    DistribMulAction Gal(L / K) (chosenNormalBasisLatticeSuccQuot K L n) where
  smul τ q := galoisGroupChosenNormalBasisLatticeSuccQuotAddEquiv K L n τ q
  one_smul := by
    intro q
    change galoisGroupChosenNormalBasisLatticeSuccQuotAddEquiv K L n 1 q = q
    let e := chosenNormalBasisLatticeSuccQuotToIntegerLatticeQuotLinearEquiv K L n
    apply e.injective
    rw [chosenNormalBasisLatticeSuccQuotToIntegerLatticeQuotLinearEquiv_galoisGroup]
    refine Submodule.Quotient.induction_on
      (chosenNormalBasisIntegerLatticeUniformizerSubmodule K L) (e q) ?_
    intro x
    rw [galoisGroupChosenNormalBasisIntegerLatticeQuotLinearEquiv_mk,
      galoisGroupChosenNormalBasisIntegerLatticeLinearEquiv_one_apply]
  mul_smul := by
    intro τ υ q
    change galoisGroupChosenNormalBasisLatticeSuccQuotAddEquiv K L n (τ * υ) q =
      galoisGroupChosenNormalBasisLatticeSuccQuotAddEquiv K L n τ
        (galoisGroupChosenNormalBasisLatticeSuccQuotAddEquiv K L n υ q)
    let e := chosenNormalBasisLatticeSuccQuotToIntegerLatticeQuotLinearEquiv K L n
    apply e.injective
    rw [chosenNormalBasisLatticeSuccQuotToIntegerLatticeQuotLinearEquiv_galoisGroup,
      chosenNormalBasisLatticeSuccQuotToIntegerLatticeQuotLinearEquiv_galoisGroup,
      chosenNormalBasisLatticeSuccQuotToIntegerLatticeQuotLinearEquiv_galoisGroup]
    refine Submodule.Quotient.induction_on
      (chosenNormalBasisIntegerLatticeUniformizerSubmodule K L) (e q) ?_
    intro x
    rw [galoisGroupChosenNormalBasisIntegerLatticeQuotLinearEquiv_mk,
      galoisGroupChosenNormalBasisIntegerLatticeQuotLinearEquiv_mk,
      galoisGroupChosenNormalBasisIntegerLatticeQuotLinearEquiv_mk,
      galoisGroupChosenNormalBasisIntegerLatticeLinearEquiv_mul_apply]
  smul_zero := by
    intro τ
    exact (galoisGroupChosenNormalBasisLatticeSuccQuotAddEquiv K L n τ).map_zero
  smul_add := by
    intro τ q r
    exact (galoisGroupChosenNormalBasisLatticeSuccQuotAddEquiv K L n τ).map_add q r

theorem galoisGroupChosenNormalBasisLatticeSuccQuotDistribMulAction_smul_mk_mulPow
    (n : Nat) (τ : Gal(L/K)) (x : chosenNormalBasisIntegerLattice K L) :
    letI := galoisGroupChosenNormalBasisLatticeSuccQuotDistribMulAction K L n
    τ • chosenNormalBasisLatticeSuccQuotMk K L n
        (chosenNormalBasisIntegerLatticeMulPowLinearEquiv K L n x) =
      chosenNormalBasisLatticeSuccQuotMk K L n
        (chosenNormalBasisIntegerLatticeMulPowLinearEquiv K L n
          (galoisGroupChosenNormalBasisIntegerLatticeLinearEquiv K L τ x)) :=
  galoisGroupChosenNormalBasisLatticeSuccQuotAddEquiv_mk_mulPow K L n τ x

theorem chosenNormalBasisLatticeSuccQuotRightRegularAddEquiv_commutes
    (n : Nat) (τ : Gal(L/K))
    (q : chosenNormalBasisLatticeSuccQuot K L n) (σ : Gal(L/K)) :
    letI := galoisGroupChosenNormalBasisLatticeSuccQuotDistribMulAction K L n
    chosenNormalBasisLatticeSuccQuotRightRegularAddEquiv K L n (τ • q) σ =
      chosenNormalBasisLatticeSuccQuotRightRegularAddEquiv K L n q (σ * τ) := by
  let := galoisGroupChosenNormalBasisLatticeSuccQuotDistribMulAction K L n
  refine chosenNormalBasisLatticeSuccQuot.inductionOn K L n
    (motive := fun q =>
      chosenNormalBasisLatticeSuccQuotRightRegularAddEquiv K L n (τ • q) σ =
        chosenNormalBasisLatticeSuccQuotRightRegularAddEquiv K L n q (σ * τ))
    q ?_
  intro z
  let x : chosenNormalBasisIntegerLattice K L :=
    (chosenNormalBasisIntegerLatticeMulPowLinearEquiv K L n).symm z
  have hz : chosenNormalBasisIntegerLatticeMulPowLinearEquiv K L n x = z :=
    (chosenNormalBasisIntegerLatticeMulPowLinearEquiv K L n).apply_symm_apply z
  rw [← hz,
    galoisGroupChosenNormalBasisLatticeSuccQuotDistribMulAction_smul_mk_mulPow,
    chosenNormalBasisLatticeSuccQuotRightRegularAddEquiv_mk_mulPow,
    chosenNormalBasisLatticeSuccQuotRightRegularAddEquiv_mk_mulPow,
    chosenNormalBasisIntegerLatticeBasis_equivFun_galoisGroup]
  congr 1

theorem chosenNormalBasisLatticeSuccQuot_herbrandH0_subsingleton (n : Nat) :
    letI := galoisGroupChosenNormalBasisLatticeSuccQuotDistribMulAction K L n
    letI :=
      (open CyclicCohomology.ProfiniteCohomology.Herbrand in
        multiplicativeMulDistribMulActionOfDistribMulAction)
        Gal(L / K) (chosenNormalBasisLatticeSuccQuot K L n)
    Subsingleton (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0
      Gal(L / K) (Multiplicative (chosenNormalBasisLatticeSuccQuot K L n))) := by
  let := galoisGroupChosenNormalBasisLatticeSuccQuotDistribMulAction K L n
  exact
    (open CyclicCohomology.ProfiniteCohomology.Herbrand in
      herbrandH0_subsingleton_of_addEquiv_rightRegularFunction
        (G := Gal(L / K)) (M := chosenNormalBasisLatticeSuccQuot K L n) (D := 𝓀[K])
        (chosenNormalBasisLatticeSuccQuotRightRegularAddEquiv K L n)
        (chosenNormalBasisLatticeSuccQuotRightRegularAddEquiv_commutes K L n))

theorem chosenNormalBasisLatticeSuccQuot_herbrandHMinusOne_subsingleton
    (n : Nat) (τ : Gal(L/K))
    (hgen : ∀ g : Gal(L / K), g ∈ Subgroup.zpowers τ) :
    letI := galoisGroupChosenNormalBasisLatticeSuccQuotDistribMulAction K L n
    letI :=
      (open CyclicCohomology.ProfiniteCohomology.Herbrand in
        multiplicativeMulDistribMulActionOfDistribMulAction)
        Gal(L / K) (chosenNormalBasisLatticeSuccQuot K L n)
    Subsingleton (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne
      Gal(L / K) (Multiplicative (chosenNormalBasisLatticeSuccQuot K L n)) τ) := by
  let := galoisGroupChosenNormalBasisLatticeSuccQuotDistribMulAction K L n
  exact
    (open CyclicCohomology.ProfiniteCohomology.Herbrand in
      herbrandHMinusOne_subsingleton_of_addEquiv_rightRegularFunction
        (G := Gal(L / K)) (M := chosenNormalBasisLatticeSuccQuot K L n) (D := 𝓀[K])
        τ hgen (chosenNormalBasisLatticeSuccQuotRightRegularAddEquiv K L n)
        (chosenNormalBasisLatticeSuccQuotRightRegularAddEquiv_commutes K L n))