import Mathlib
import Definitions.Def_ClassGroup_ModP

set_option autoImplicit false

open scoped NumberField nonZeroDivisors
open Polynomial

section Fidl
variable {R : Type*} [CommRing R] [IsDomain R]
variable {R' : Type*} [CommRing R'] [IsDomain R']
variable (K : Type*) [Field K] [Algebra R K] [IsFractionRing R K]
variable (L : Type*) [Field L] [Algebra R' L] [IsFractionRing R' L]

theorem FractionalIdeal.ringEquivOfRingEquiv_coeIdeal (g : R ≃+* R') (I : Ideal R) :
    FractionalIdeal.ringEquivOfRingEquiv K L g (I : FractionalIdeal R⁰ K) =
      ((I.map (g : R →+* R') : Ideal R') : FractionalIdeal R'⁰ L) := by
  ext x
  rw [← FractionalIdeal.mem_coe, ← FractionalIdeal.mem_coe,
    FractionalIdeal.ringEquivOfRingEquiv_apply, FractionalIdeal.coe_mk,
    FractionalIdeal.val_eq_coe]
  simp only [Submodule.mem_map, FractionalIdeal.mem_coe, FractionalIdeal.mem_coeIdeal]
  constructor
  · rintro ⟨-, ⟨a, haI, rfl⟩, rfl⟩
    exact ⟨g a, Ideal.mem_map_of_mem _ haI,
      by rw [LinearEquiv.coe_coe, IsFractionRing.semilinearEquivOfRingEquiv_apply,
        IsFractionRing.ringEquivOfRingEquiv_algebraMap]⟩
  · rintro ⟨b, hbI, rfl⟩
    obtain ⟨a, haI, rfl⟩ := (Ideal.mem_map_iff_of_surjective _ g.surjective).mp hbI
    exact ⟨algebraMap R K a, ⟨a, haI, rfl⟩,
      by rw [LinearEquiv.coe_coe, IsFractionRing.semilinearEquivOfRingEquiv_apply,
        IsFractionRing.ringEquivOfRingEquiv_algebraMap]⟩

end Fidl

section ClassGroupFunctoriality
variable {R : Type*} [CommRing R] [IsDomain R]
variable {R' : Type*} [CommRing R'] [IsDomain R']

theorem ClassGroup.mulEquiv_mk_eq_mk (g : R ≃+* R')
    {I : (FractionalIdeal R⁰ (FractionRing R))ˣ}
    {J : (FractionalIdeal R'⁰ (FractionRing R'))ˣ}
    (hIJ : FractionalIdeal.ringEquivOfRingEquiv (FractionRing R) (FractionRing R') g
        (I : FractionalIdeal R⁰ (FractionRing R)) = (J : FractionalIdeal R'⁰ (FractionRing R'))) :
    ClassGroup.mulEquiv g (ClassGroup.mk _ I) = ClassGroup.mk _ J := by
  have hself : ∀ (J' : (FractionalIdeal R'⁰ (FractionRing R'))ˣ),
      ClassGroup.equiv (R := R') (FractionRing R') (ClassGroup.mk _ J') =
        QuotientGroup.mk' _ J' := by
    intro J'
    rw [ClassGroup.equiv_mk]
    congr 1
    rw [← Units.val_inj, Units.coe_mapEquiv]
    simp [FractionalIdeal.canonicalEquiv_self]
  rw [ClassGroup.mulEquiv, MulEquiv.trans_apply, MulEquiv.trans_apply, ClassGroup.equiv_mk,
    show Units.mapEquiv (↑(FractionalIdeal.canonicalEquiv R⁰ (FractionRing R) (FractionRing R)))
        I = I by
      rw [← Units.val_inj, Units.coe_mapEquiv]
      simp [FractionalIdeal.canonicalEquiv_self],
    QuotientGroup.congr_mk']
  rw [MulEquiv.symm_apply_eq, hself]
  congr 1
  rw [← Units.val_inj, Units.coe_mapEquiv]
  exact hIJ

def Ideal.mapNonZero (g : R ≃+* R') (P : (Ideal R)⁰) : (Ideal R')⁰ :=
  ⟨(P : Ideal R).map (g : R →+* R'), by
    have hinj : Function.Injective ((g : R →+* R') : R → R') := g.injective
    refine mem_nonZeroDivisors_iff_ne_zero.mpr fun hbot => ?_
    refine mem_nonZeroDivisors_iff_ne_zero.mp P.2 ?_
    rw [Ideal.zero_eq_bot] at hbot ⊢
    exact (Ideal.map_eq_bot_iff_of_injective hinj).mp hbot⟩

@[simp] lemma Ideal.coe_mapNonZero (g : R ≃+* R') (P : (Ideal R)⁰) :
    (Ideal.mapNonZero g P : Ideal R') = (P : Ideal R).map (g : R →+* R') := rfl

variable [IsDedekindDomain R] [IsDedekindDomain R']

theorem ClassGroup.mulEquiv_mk0 (g : R ≃+* R') (P : (Ideal R)⁰) :
    ClassGroup.mulEquiv g (ClassGroup.mk0 P) = ClassGroup.mk0 (Ideal.mapNonZero g P) := by
  show ClassGroup.mulEquiv g (ClassGroup.mk _ (FractionalIdeal.mk0 (FractionRing R) P)) =
    ClassGroup.mk _ (FractionalIdeal.mk0 (FractionRing R') (Ideal.mapNonZero g P))
  refine ClassGroup.mulEquiv_mk_eq_mk g ?_
  rw [FractionalIdeal.coe_mk0, FractionalIdeal.coe_mk0,
    FractionalIdeal.ringEquivOfRingEquiv_coeIdeal, Ideal.coe_mapNonZero]

theorem ClassGroup.mulEquiv_refl_apply (C : ClassGroup R) :
    ClassGroup.mulEquiv (RingEquiv.refl R) C = C := by
  obtain ⟨P, rfl⟩ := ClassGroup.mk0_surjective C
  rw [ClassGroup.mulEquiv_mk0]
  congr 1
  refine Subtype.ext ?_
  rw [Ideal.coe_mapNonZero,
    show ((RingEquiv.refl R : R ≃+* R) : R →+* R) = RingHom.id R from RingHom.ext fun _ => rfl,
    Ideal.map_id]

theorem ClassGroup.mulEquiv_trans_apply {R'' : Type*} [CommRing R''] [IsDomain R'']
    [IsDedekindDomain R''] (g : R ≃+* R') (h : R' ≃+* R'') (C : ClassGroup R) :
    ClassGroup.mulEquiv (g.trans h) C = ClassGroup.mulEquiv h (ClassGroup.mulEquiv g C) := by
  obtain ⟨P, rfl⟩ := ClassGroup.mk0_surjective C
  rw [ClassGroup.mulEquiv_mk0, ClassGroup.mulEquiv_mk0, ClassGroup.mulEquiv_mk0]
  congr 1
  refine Subtype.ext ?_
  rw [Ideal.coe_mapNonZero, Ideal.coe_mapNonZero, Ideal.coe_mapNonZero,
    show ((g.trans h : R ≃+* R'') : R →+* R'') = (h : R' →+* R'').comp (g : R →+* R') from
      RingHom.ext fun _ => rfl,
    ← Ideal.map_map]

end ClassGroupFunctoriality

section GalRestrict

def algAutToRingAut (A B : Type*) [CommSemiring A] [Semiring B] [Algebra A B] :
    (B ≃ₐ[A] B) →* (B ≃+* B) where
  toFun := AlgEquiv.toRingEquiv
  map_one' := RingEquiv.ext fun _ => rfl
  map_mul' _ _ := RingEquiv.ext fun _ => rfl

@[simp] lemma algAutToRingAut_apply {A B : Type*} [CommSemiring A] [Semiring B] [Algebra A B]
    (e : B ≃ₐ[A] B) (x : B) : algAutToRingAut A B e x = e x := rfl

variable (A K L B : Type*) [CommRing A] [CommRing B] [Algebra A B]
  [Field K] [Field L] [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra.IsAlgebraic K L]
  [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L]

noncomputable def galRestrictionDatum : (L ≃ₐ[K] L) →* (B ≃+* B) :=
  (algAutToRingAut A B).comp (galRestrict A K L B).toMonoidHom

@[simp] lemma galRestrictionDatum_apply (g : L ≃ₐ[K] L) (x : B) :
    galRestrictionDatum A K L B g x = galRestrict A K L B g x := rfl

end GalRestrict

namespace JacobiSumStickelberger

section ClassGroupCarrier

variable (p : ℕ) [NeZero p]

section DedekindAction

variable (R : Type*) [CommRing R] [IsDomain R]

variable {R} in
variable [IsDedekindDomain R] in

theorem clEnd_clProj_mk0 (g : R ≃+* R) (P : (Ideal R)⁰) :
    clEnd p g (clProj p R (Additive.ofMul (ClassGroup.mk0 P))) =
      clProj p R (Additive.ofMul (ClassGroup.mk0 (Ideal.mapNonZero g P))) := by
  rw [clEnd_clProj, ClassGroup.mulEquiv_mk0]

variable {R} in
variable [IsDedekindDomain R] in

noncomputable def clEndHom : (R ≃+* R) →* Module.End (ZMod p) (ClGalModule p R) where
  toFun := clEnd p
  map_one' := by
    refine LinearMap.ext fun a => ?_
    obtain ⟨C, rfl⟩ := clProj_surjective p R a
    rw [Module.End.one_apply]
    show clProj p R (Additive.ofMul (ClassGroup.mulEquiv (RingEquiv.refl R) C.toMul)) =
      clProj p R C
    rw [ClassGroup.mulEquiv_refl_apply]; rfl
  map_mul' g h := by
    refine LinearMap.ext fun a => ?_
    obtain ⟨C, rfl⟩ := clProj_surjective p R a
    rw [Module.End.mul_apply]
    show clProj p R (Additive.ofMul (ClassGroup.mulEquiv (h.trans g) C.toMul)) =
      clEnd p g (clProj p R (Additive.ofMul (ClassGroup.mulEquiv h C.toMul)))
    rw [clEnd_clProj, ClassGroup.mulEquiv_trans_apply]

end DedekindAction

section Cyclotomic

variable (K : Type*) [Field K] [NumberField K]

noncomputable def cycloGalEquiv [IsCyclotomicExtension {p} ℚ K] :
    (K ≃ₐ[ℚ] K) ≃* (ZMod p)ˣ :=
  IsCyclotomicExtension.autEquivPow K
    (Polynomial.cyclotomic.irreducible_rat (Nat.pos_of_ne_zero (NeZero.ne p)))

noncomputable def clRingAction [IsCyclotomicExtension {p} ℚ K] :
    (ZMod p)ˣ →* ((𝓞 K) ≃+* (𝓞 K)) :=
  (galRestrictionDatum ℤ ℚ K (𝓞 K)).comp (cycloGalEquiv p K).symm.toMonoidHom

noncomputable def clGalAction [IsCyclotomicExtension {p} ℚ K] :
    (ZMod p)ˣ →* Module.End (ZMod p) (ClGalModule p (𝓞 K)) :=
  (clEndHom p).comp (clRingAction p K)

theorem clGalAction_clProj_mk0 [IsCyclotomicExtension {p} ℚ K] (d : (ZMod p)ˣ)
    (P : (Ideal (𝓞 K))⁰) :
    clGalAction p K d (clProj p (𝓞 K) (Additive.ofMul (ClassGroup.mk0 P))) =
      clProj p (𝓞 K) (Additive.ofMul (ClassGroup.mk0
        (Ideal.mapNonZero (clRingAction p K d) P))) :=
  clEnd_clProj_mk0 p (clRingAction p K d) P

end Cyclotomic

end ClassGroupCarrier

end JacobiSumStickelberger