import Definitions.Def_CompletionInvariants
import Definitions.Def_SemilocalAdicCompletion

universe u₁ u₂ u₃

open Pointwise
open scoped TensorProduct

namespace AdicCompletion

variable (A : Type u₁) (B : Type u₂) [CommRing A] [CommRing B] [Algebra A B]
variable (G : Type u₃) [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
variable (𝔭 : Ideal A)

section FibreIndex

variable [𝔭.IsMaximal]

theorem liesOver_of_isPrime_of_map_le (Q : Ideal B) [hQp : Q.IsPrime]
    (hQ : 𝔭.map (algebraMap A B) ≤ Q) : Q.LiesOver 𝔭 := by
  constructor
  have h1 : 𝔭 ≤ Q.under A := Ideal.map_le_iff_le_comap.mp hQ
  have h2 : Q.under A ≠ ⊤ := Ideal.comap_ne_top _ hQp.ne_top
  exact ‹𝔭.IsMaximal›.eq_of_le h2 h1

omit [𝔭.IsMaximal] in
theorem under_eq_of_liesOver (Q : Ideal B) [h : Q.LiesOver 𝔭] :
    Q.comap (algebraMap A B) = 𝔭 := by
  rw [← Ideal.under_def]
  exact (Ideal.over_def Q 𝔭).symm

omit [𝔭.IsMaximal] in
theorem map_le_of_liesOver (Q : Ideal B) [Q.LiesOver 𝔭] :
    𝔭.map (algebraMap A B) ≤ Q :=
  Ideal.map_le_iff_le_comap.mpr (le_of_eq (under_eq_of_liesOver A B 𝔭 Q).symm)

variable [Finite G] [Algebra.IsInvariant A B G]

include G in
omit [SMulCommClass G A B] in
theorem isMaximal_of_isPrime_of_liesOver (Q : Ideal B) [Q.IsPrime] [Q.LiesOver 𝔭] :
    Q.IsMaximal := by
  haveI := Algebra.IsInvariant.isIntegral A B G
  refine Ideal.isMaximal_of_isIntegral_of_isMaximal_comap (R := A) Q ?_
  rw [under_eq_of_liesOver A B 𝔭 Q]
  infer_instance

include G in
omit [SMulCommClass G A B] in

theorem isMaximal_and_map_le_iff (Q : Ideal B) :
    (Q.IsMaximal ∧ 𝔭.map (algebraMap A B) ≤ Q) ↔ Q ∈ 𝔭.primesOver B := by
  constructor
  · rintro ⟨hmax, hle⟩
    haveI := hmax.isPrime
    exact ⟨hmax.isPrime, liesOver_of_isPrime_of_map_le A B 𝔭 Q hle⟩
  · rintro ⟨hprime, hover⟩
    haveI := hprime
    haveI := hover
    exact ⟨isMaximal_of_isPrime_of_liesOver A B G 𝔭 Q, map_le_of_liesOver A B 𝔭 Q⟩

omit [𝔭.IsMaximal] in

theorem exists_smul_eq_of_liesOver (Q Q' : Ideal B) [Q.IsPrime] [Q.LiesOver 𝔭]
    [Q'.IsPrime] [Q'.LiesOver 𝔭] : ∃ g : G, Q' = g • Q := by
  refine Algebra.IsInvariant.exists_smul_of_under_eq A B G Q Q' ?_
  rw [← Ideal.over_def Q 𝔭, ← Ideal.over_def Q' 𝔭]

end FibreIndex

section Transport

theorem map_toAlgEquiv_le_of_smul_le {𝔓 Q : Ideal B} (g : G) (h : g • 𝔓 ≤ Q) :
    𝔓.map (MulSemiringAction.toAlgEquiv A B g : B →ₐ[A] B) ≤ Q := by
  refine le_trans (le_of_eq ?_) h
  rw [Ideal.pointwise_smul_def]
  rfl

noncomputable def transportOf (g : G) {𝔓 Q : Ideal B} (h : g • 𝔓 ≤ Q) :
    AdicCompletion 𝔓 B →ₐ[A] AdicCompletion Q B :=
  mapₐ 𝔓 Q (MulSemiringAction.toAlgEquiv A B g : B →ₐ[A] B)
    (map_toAlgEquiv_le_of_smul_le A B G g h)

theorem evalₐ_transportOf (g : G) {𝔓 Q : Ideal B} (h : g • 𝔓 ≤ Q) (n : ℕ)
    (x : AdicCompletion 𝔓 B) (z : B)
    (hz : Ideal.Quotient.mk (𝔓 ^ n) z = evalₐ 𝔓 n x) :
    evalₐ Q n (transportOf A B G g h x) = Ideal.Quotient.mk (Q ^ n) (g • z) := by
  rw [transportOf, evalₐ_mapₐ, ← hz, levelMapₐ_mk]
  rfl

@[simp]
theorem transportOf_of (g : G) {𝔓 Q : Ideal B} (h : g • 𝔓 ≤ Q) (b : B) :
    transportOf A B G g h (of 𝔓 B b) = of Q B (g • b) := by
  rw [transportOf, mapₐ_of]
  rfl

theorem transportOf_eq_of_fixed {𝔓 Q : Ideal B} (g g' : G) (hg : g • 𝔓 = Q)
    (hg' : g' • 𝔓 = Q) (y : AdicCompletion 𝔓 B)
    (hy : ∀ h : MulAction.stabilizer G 𝔓, stabAut A B G 𝔓 h y = y) :
    transportOf A B G g hg.le y = transportOf A B G g' hg'.le y := by
  have hmem : g'⁻¹ * g ∈ MulAction.stabilizer G 𝔓 := by
    rw [MulAction.mem_stabilizer_iff, mul_smul, hg, ← hg', inv_smul_smul]
  refine ext_evalₐ fun n => ?_
  obtain ⟨z, hz⟩ := Ideal.Quotient.mk_surjective (evalₐ 𝔓 n y)
  rw [evalₐ_transportOf A B G g hg.le n y z hz,
    evalₐ_transportOf A B G g' hg'.le n y z hz]
  have h1 : Ideal.Quotient.mk (𝔓 ^ n) ((g'⁻¹ * g) • z) = Ideal.Quotient.mk (𝔓 ^ n) z := by
    have h0 := congrArg (evalₐ 𝔓 n) (hy ⟨g'⁻¹ * g, hmem⟩)
    rw [evalₐ_stabAut A B G 𝔓 _ n y z hz, ← hz] at h0
    exact h0
  have h2 := congrArg (levelMapₐ 𝔓 Q (MulSemiringAction.toAlgEquiv A B g' : B →ₐ[A] B)
    (map_toAlgEquiv_le_of_smul_le A B G g' hg'.le) n) h1
  rw [levelMapₐ_mk, levelMapₐ_mk] at h2
  have h3 : Ideal.Quotient.mk (Q ^ n) (g' • (g'⁻¹ * g) • z) =
      Ideal.Quotient.mk (Q ^ n) (g' • z) := h2
  rwa [← mul_smul, mul_inv_cancel_left] at h3

theorem map_algebraMap_le_smul {Q : Ideal B} (g : G)
    (hQ : 𝔭.map (algebraMap A B) ≤ Q) : 𝔭.map (algebraMap A B) ≤ g • Q := by
  rw [← smul_map_algebraMap A B G 𝔭 g, Ideal.pointwise_smul_def, Ideal.pointwise_smul_def]
  exact Ideal.map_mono hQ

theorem semilocalComponent_selfSmul (g : G) {Q : Ideal B}
    (hQ : 𝔭.map (algebraMap A B) ≤ Q)
    (x : AdicCompletion (𝔭.map (algebraMap A B)) B) :
    letI := selfCompletionMulSemiringAction A B G 𝔭
    semilocalComponent (𝔭.map (algebraMap A B)) (map_algebraMap_le_smul A B G 𝔭 g hQ)
        (g • x) =
      transportOf A B G g (le_refl (g • Q)) (semilocalComponent _ hQ x) := by
  letI := selfCompletionMulSemiringAction A B G 𝔭
  refine ext_evalₐ fun n => ?_
  obtain ⟨z, hz⟩ := Ideal.Quotient.mk_surjective (evalₐ (𝔭.map (algebraMap A B)) n x)
  have hcomp : Ideal.Quotient.mk (Q ^ n) z =
      evalₐ Q n (semilocalComponent (𝔭.map (algebraMap A B)) hQ x) := by
    rw [semilocalComponent, evalₐ_mapₐ, ← hz, levelMapₐ_mk]
    rfl
  have hsmul : Ideal.Quotient.mk ((𝔭.map (algebraMap A B)) ^ n) (g • z) =
      evalₐ (𝔭.map (algebraMap A B)) n (g • x) := by
    rw [show (g • x : AdicCompletion (𝔭.map (algebraMap A B)) B) =
        stabAut A B G _ (toStabilizerExtended A B G 𝔭 g) x from rfl,
      evalₐ_stabAut A B G _ _ n x z hz]
    rfl
  rw [semilocalComponent, evalₐ_mapₐ, ← hsmul, levelMapₐ_mk,
    evalₐ_transportOf A B G g (le_refl (g • Q)) n
      (semilocalComponent (𝔭.map (algebraMap A B)) hQ x) z hcomp]
  rfl

end Transport

end AdicCompletion

section SameUniverseHead

namespace AdicCompletion

variable (A : Type u₁) (B : Type u₁) [CommRing A] [CommRing B] [Algebra A B]
variable (G : Type u₃) [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B]
variable [IsNoetherianRing A] [Module.Finite A B] [FaithfulSMul A B]
variable [Algebra.IsInvariant A B G]
variable (𝔭 : Ideal A) [𝔭.IsMaximal]

include A in
omit [FaithfulSMul A B] in

theorem isNoetherianRing_of_finite_algebra : IsNoetherianRing B :=
  isNoetherian_of_tower A (inferInstance : IsNoetherian A B)

omit [IsNoetherianRing A] [FaithfulSMul A B] in

theorem isArtinianRing_quotient_map :
    IsArtinianRing (B ⧸ 𝔭.map (algebraMap A B)) := by
  letI : DivisionRing (A ⧸ 𝔭) := Ideal.Quotient.divisionRing 𝔭
  haveI : IsArtinianRing (A ⧸ 𝔭) := inferInstance
  haveI : Module.Finite A (B ⧸ 𝔭.map (algebraMap A B)) :=
    Module.Finite.of_surjective
      (Ideal.Quotient.mkₐ A (𝔭.map (algebraMap A B))).toLinearMap
      (Ideal.Quotient.mkₐ_surjective A _)
  haveI : IsArtinian A (B ⧸ 𝔭.map (algebraMap A B)) := by
    refine isArtinian_of_finite_of_smul_eq_zero 𝔭 ?_
    rintro i hi m
    obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective m
    rw [show i • (Ideal.Quotient.mk (𝔭.map (algebraMap A B)) b) =
        Ideal.Quotient.mk (𝔭.map (algebraMap A B)) (i • b) from
      (map_smul (Ideal.Quotient.mkₐ A (𝔭.map (algebraMap A B))) i b).symm,
      Algebra.smul_def, Ideal.Quotient.eq_zero_iff_mem]
    exact Ideal.mul_mem_right _ _ (Ideal.mem_map_of_mem _ hi)
  exact isArtinian_of_tower A inferInstance

variable (𝔓 : Ideal B) [𝔓.IsPrime] [𝔓.LiesOver 𝔭]

include G in
omit [SMulCommClass G A B] [IsNoetherianRing A] [Module.Finite A B] [FaithfulSMul A B] in

theorem mem_index_self : 𝔓.IsMaximal ∧ 𝔭.map (algebraMap A B) ≤ 𝔓 :=
  (isMaximal_and_map_le_iff A B G 𝔭 𝔓).mpr ⟨inferInstance, inferInstance⟩

omit [IsNoetherianRing A] [Module.Finite A B] [FaithfulSMul A B] in

theorem smul_mem_index (g : G) {Q : Ideal B}
    (h : Q.IsMaximal ∧ 𝔭.map (algebraMap A B) ≤ Q) :
    (g • Q).IsMaximal ∧ 𝔭.map (algebraMap A B) ≤ g • Q := by
  haveI : Q.IsMaximal := h.1
  haveI hp : (g • Q).IsPrime := by
    rw [Ideal.pointwise_smul_def]
    refine Ideal.map_isPrime_of_surjective (f := MulSemiringAction.toRingHom G B g)
      (fun b => ⟨g⁻¹ • b, smul_inv_smul g b⟩) ?_
    rw [(RingHom.injective_iff_ker_eq_bot _).mp
      (fun x y hxy => by simpa using congrArg (fun t => g⁻¹ • t) hxy)]
    exact bot_le
  have hle : 𝔭.map (algebraMap A B) ≤ g • Q := map_algebraMap_le_smul A B G 𝔭 g h.2
  haveI : (g • Q).LiesOver 𝔭 := liesOver_of_isPrime_of_map_le A B 𝔭 (g • Q) hle
  exact ⟨isMaximal_of_isPrime_of_liesOver A B G 𝔭 (g • Q), hle⟩

omit [IsNoetherianRing A] [Module.Finite A B] [FaithfulSMul A B] [𝔭.IsMaximal] in

theorem completionBaseChangeHom_eq_tensor (x : AdicCompletion 𝔭 A) :
    completionBaseChangeHom B 𝔭 x = tensorRingHom B 𝔭 (x ⊗ₜ[A] 1) := by
  have h : of (𝔭.map (algebraMap A B)) B (1 : B) = 1 :=
    map_one (completionOfAlgHom B 𝔭)
  rw [tensorRingHom_tmul, h, mul_one]

omit [𝔭.IsMaximal] in
theorem completionBaseChangeHom_injective :
    Function.Injective (completionBaseChangeHom B 𝔭) := by
  intro x y hxy
  rw [completionBaseChangeHom_eq_tensor, completionBaseChangeHom_eq_tensor] at hxy
  exact Algebra.TensorProduct.includeLeft_injective (S := A)
    (FaithfulSMul.algebraMap_injective A B)
    ((tensorRingHom_bijective B 𝔭).injective hxy)

include G in

noncomputable def invariantsCompletionHom :
    AdicCompletion 𝔭 A →ₐ[A] AdicCompletion 𝔓 B :=
  ((semilocalComponent (𝔭.map (algebraMap A B))
      (mem_index_self A B G 𝔭 𝔓).2).restrictScalars A).comp
    (completionBaseChangeHom B 𝔭)

include G in
omit [SMulCommClass G A B] [IsNoetherianRing A] [Module.Finite A B] [FaithfulSMul A B] in
theorem evalₐ_invariantsCompletionHom (a : AdicCauchySequence 𝔭 A) (n : ℕ) :
    evalₐ 𝔓 n (invariantsCompletionHom A B G 𝔭 𝔓 (mk 𝔭 A a)) =
      Ideal.Quotient.mk (𝔓 ^ n) (algebraMap A B (a.val n)) := by
  show evalₐ 𝔓 n (semilocalComponent (𝔭.map (algebraMap A B))
      (mem_index_self A B G 𝔭 𝔓).2 (completionBaseChangeHom B 𝔭 (mk 𝔭 A a))) = _
  have hbc : Ideal.Quotient.mk ((𝔭.map (algebraMap A B)) ^ n)
      (algebraMap A B (a.val n)) =
      evalₐ (𝔭.map (algebraMap A B)) n (completionBaseChangeHom B 𝔭 (mk 𝔭 A a)) := by
    simp [completionBaseChangeHom, Algebra.ofId_apply]
  rw [semilocalComponent, evalₐ_mapₐ, ← hbc, levelMapₐ_mk]
  rfl

omit [IsNoetherianRing A] [Module.Finite A B] [FaithfulSMul A B] in

theorem stabAut_invariantsCompletionHom (h : MulAction.stabilizer G 𝔓)
    (x : AdicCompletion 𝔭 A) :
    stabAut A B G 𝔓 h (invariantsCompletionHom A B G 𝔭 𝔓 x) =
      invariantsCompletionHom A B G 𝔭 𝔓 x := by
  induction x using AdicCompletion.induction_on with
  | _ a =>
    refine ext_evalₐ fun n => ?_
    rw [evalₐ_stabAut A B G 𝔓 h n _ _
        (evalₐ_invariantsCompletionHom A B G 𝔭 𝔓 a n).symm,
      smul_algebraMap, evalₐ_invariantsCompletionHom]

omit [FaithfulSMul A B] in

theorem eq_of_component_eq_of_smul_eq
    (w w' : AdicCompletion (𝔭.map (algebraMap A B)) B)
    (hw : ∀ g : G, stabAut A B G _ (toStabilizerExtended A B G 𝔭 g) w = w)
    (hw' : ∀ g : G, stabAut A B G _ (toStabilizerExtended A B G 𝔭 g) w' = w')
    (h𝔓 : semilocalComponent (𝔭.map (algebraMap A B))
        (mem_index_self A B G 𝔭 𝔓).2 w =
      semilocalComponent (𝔭.map (algebraMap A B)) (mem_index_self A B G 𝔭 𝔓).2 w') :
    w = w' := by
  haveI := isNoetherianRing_of_finite_algebra A B
  haveI := isArtinianRing_quotient_map A B 𝔭
  apply semilocalPiHom_injective (𝔭.map (algebraMap A B))
  funext P
  obtain ⟨Q, hQ⟩ := P
  haveI : Q.IsPrime := hQ.1.isPrime
  haveI : Q.LiesOver 𝔭 := liesOver_of_isPrime_of_map_le A B 𝔭 Q hQ.2
  obtain ⟨g, hg⟩ := exists_smul_eq_of_liesOver A B G 𝔭 𝔓 Q
  subst hg
  show semilocalComponent _ hQ.2 w = semilocalComponent _ hQ.2 w'
  calc semilocalComponent _ hQ.2 w
      = semilocalComponent _ hQ.2
          (stabAut A B G _ (toStabilizerExtended A B G 𝔭 g) w) := by rw [hw g]
    _ = transportOf A B G g (le_refl (g • 𝔓))
          (semilocalComponent _ (mem_index_self A B G 𝔭 𝔓).2 w) :=
        semilocalComponent_selfSmul A B G 𝔭 g (mem_index_self A B G 𝔭 𝔓).2 w
    _ = transportOf A B G g (le_refl (g • 𝔓))
          (semilocalComponent _ (mem_index_self A B G 𝔭 𝔓).2 w') := by rw [h𝔓]
    _ = semilocalComponent _ hQ.2
          (stabAut A B G _ (toStabilizerExtended A B G 𝔭 g) w') :=
        (semilocalComponent_selfSmul A B G 𝔭 g (mem_index_self A B G 𝔭 𝔓).2 w').symm
    _ = semilocalComponent _ hQ.2 w' := by rw [hw' g]

omit [Finite G] [IsNoetherianRing A] [Module.Finite A B] [FaithfulSMul A B]
  [Algebra.IsInvariant A B G] in

theorem transportOf_one (J : Ideal B) (y : AdicCompletion J B) :
    transportOf A B G 1 ((one_smul G J).le) y = y := by
  refine ext_evalₐ fun n => ?_
  obtain ⟨z, hz⟩ := Ideal.Quotient.mk_surjective (evalₐ J n y)
  rw [evalₐ_transportOf A B G 1 ((one_smul G J).le) n y z hz, one_smul, hz]

omit [Finite G] [IsNoetherianRing A] [Module.Finite A B] [FaithfulSMul A B]
  [Algebra.IsInvariant A B G] [𝔭.IsMaximal] in

theorem evalₐ_component_selfSmul (g : G) {Q : Ideal B}
    (hQ : 𝔭.map (algebraMap A B) ≤ Q)
    (x : AdicCompletion (𝔭.map (algebraMap A B)) B) (n : ℕ) (z : B)
    (hz : Ideal.Quotient.mk ((𝔭.map (algebraMap A B)) ^ n) z =
      evalₐ (𝔭.map (algebraMap A B)) n x) :
    evalₐ Q n (semilocalComponent (𝔭.map (algebraMap A B)) hQ
        (stabAut A B G _ (toStabilizerExtended A B G 𝔭 g) x)) =
      Ideal.Quotient.mk (Q ^ n) (g • z) := by
  have hsmul : Ideal.Quotient.mk ((𝔭.map (algebraMap A B)) ^ n) (g • z) =
      evalₐ (𝔭.map (algebraMap A B)) n
        (stabAut A B G _ (toStabilizerExtended A B G 𝔭 g) x) := by
    rw [evalₐ_stabAut A B G _ _ n x z hz]
    rfl
  rw [semilocalComponent, evalₐ_mapₐ, ← hsmul, levelMapₐ_mk]
  rfl

omit [IsNoetherianRing A] [Module.Finite A B] [FaithfulSMul A B] [𝔭.IsMaximal] in

theorem evalₐ_component {Q : Ideal B} (hQ : 𝔭.map (algebraMap A B) ≤ Q)
    (x : AdicCompletion (𝔭.map (algebraMap A B)) B) (n : ℕ) (z : B)
    (hz : Ideal.Quotient.mk ((𝔭.map (algebraMap A B)) ^ n) z =
      evalₐ (𝔭.map (algebraMap A B)) n x) :
    evalₐ Q n (semilocalComponent (𝔭.map (algebraMap A B)) hQ x) =
      Ideal.Quotient.mk (Q ^ n) z := by
  rw [semilocalComponent, evalₐ_mapₐ, ← hz, levelMapₐ_mk]
  rfl

include G in

theorem invariantsCompletionHom_injective :
    Function.Injective (invariantsCompletionHom A B G 𝔭 𝔓) := by
  intro x y hxy
  refine completionBaseChangeHom_injective A B 𝔭 ?_
  refine eq_of_component_eq_of_smul_eq A B G 𝔭 𝔓 _ _
    (fun g => selfCompletion_smul_completionBaseChangeHom A B G 𝔭 g x)
    (fun g => selfCompletion_smul_completionBaseChangeHom A B G 𝔭 g y) hxy

omit [FaithfulSMul A B] in

theorem exists_invariantsCompletionHom_eq (y : AdicCompletion 𝔓 B)
    (hy : ∀ h : MulAction.stabilizer G 𝔓, stabAut A B G 𝔓 h y = y) :
    ∃ x : AdicCompletion 𝔭 A, invariantsCompletionHom A B G 𝔭 𝔓 x = y := by
  haveI := isNoetherianRing_of_finite_algebra A B
  haveI := isArtinianRing_quotient_map A B 𝔭

  have hch : ∀ P : {Q : Ideal B // Q.IsMaximal ∧ 𝔭.map (algebraMap A B) ≤ Q},
      ∃ g : G, (P : Ideal B) = g • 𝔓 := by
    rintro ⟨Q, hQ⟩
    haveI : Q.IsPrime := hQ.1.isPrime
    haveI : Q.LiesOver 𝔭 := liesOver_of_isPrime_of_map_le A B 𝔭 Q hQ.2
    exact exists_smul_eq_of_liesOver A B G 𝔭 𝔓 Q
  choose gO hgO using hch
  set w : AdicCompletion (𝔭.map (algebraMap A B)) B :=
    (semilocalPiEquiv (𝔭.map (algebraMap A B))).symm
      (fun P => transportOf A B G (gO P) (hgO P).ge y) with hw
  have hwF : ∀ P : {Q : Ideal B // Q.IsMaximal ∧ 𝔭.map (algebraMap A B) ≤ Q},
      semilocalComponent (𝔭.map (algebraMap A B)) P.2.2 w =
        transportOf A B G (gO P) (hgO P).ge y := fun P =>
    congrFun ((semilocalPiEquiv (𝔭.map (algebraMap A B))).apply_symm_apply _) P

  have hwfix : ∀ g : G, stabAut A B G _ (toStabilizerExtended A B G 𝔭 g) w = w := by
    intro g
    apply semilocalPiHom_injective (𝔭.map (algebraMap A B))
    funext P
    show semilocalComponent _ P.2.2 _ = semilocalComponent _ P.2.2 w
    rw [hwF P]
    refine ext_evalₐ fun n => ?_
    obtain ⟨z, hz⟩ := Ideal.Quotient.mk_surjective
      (evalₐ (𝔭.map (algebraMap A B)) n w)
    obtain ⟨u, hu⟩ := Ideal.Quotient.mk_surjective (evalₐ 𝔓 n y)

    set P' : {Q : Ideal B // Q.IsMaximal ∧ 𝔭.map (algebraMap A B) ≤ Q} :=
      ⟨g⁻¹ • (P : Ideal B), smul_mem_index A B G 𝔭 g⁻¹ P.2⟩ with hP'

    have h1 : Ideal.Quotient.mk ((g⁻¹ • (P : Ideal B)) ^ n) z =
        Ideal.Quotient.mk ((g⁻¹ • (P : Ideal B)) ^ n) (gO P' • u) := by
      have hc := congrArg (evalₐ (g⁻¹ • (P : Ideal B)) n) (hwF P')
      rw [evalₐ_component A B 𝔭 P'.2.2 w n z hz] at hc
      exact hc.trans (evalₐ_transportOf A B G (gO P') (hgO P').ge n y u hu)

    have h2 := congrArg (levelMapₐ (g⁻¹ • (P : Ideal B)) (P : Ideal B)
      (MulSemiringAction.toAlgEquiv A B g : B →ₐ[A] B)
      (map_toAlgEquiv_le_of_smul_le A B G g (smul_inv_smul g (P : Ideal B)).le) n) h1
    rw [levelMapₐ_mk, levelMapₐ_mk] at h2
    have h3 : Ideal.Quotient.mk ((P : Ideal B) ^ n) (g • z) =
        Ideal.Quotient.mk ((P : Ideal B) ^ n) (g • gO P' • u) := h2

    have hco : transportOf A B G (g * gO P')
        (show (g * gO P') • 𝔓 = (P : Ideal B) from by
          rw [mul_smul, ← (hgO P'), smul_inv_smul]).le y =
        transportOf A B G (gO P) ((hgO P).symm).le y :=
      transportOf_eq_of_fixed A B G (g * gO P') (gO P)
        (by rw [mul_smul, ← (hgO P'), smul_inv_smul]) (hgO P).symm y hy
    have h4 := congrArg (evalₐ (P : Ideal B) n) hco
    rw [evalₐ_transportOf A B G (g * gO P') _ n y u hu,
      evalₐ_transportOf A B G (gO P) _ n y u hu, mul_smul] at h4

    rw [evalₐ_component_selfSmul A B G 𝔭 g P.2.2 w n z hz,
      evalₐ_transportOf A B G (gO P) (hgO P).ge n y u hu]
    exact h3.trans h4

  set z' : AdicCompletion 𝔭 A ⊗[A] B := (tensorRingEquiv B 𝔭).symm w with hz'
  have hz'fix : ∀ g : G,
      (letI := Algebra.TensorProduct.rightMulSemiringAction A (AdicCompletion 𝔭 A) B G
      g • z') = z' := by
    intro g
    letI := Algebra.TensorProduct.rightMulSemiringAction A (AdicCompletion 𝔭 A) B G
    refine (tensorRingHom_bijective B 𝔭).injective ?_
    have he := tensorRingHom_equivariant A B G 𝔭 g z'
    rw [he, show tensorRingHom B 𝔭 z' = w from (tensorRingEquiv B 𝔭).apply_symm_apply w]
    exact hwfix g
  haveI := Algebra.IsInvariant.isInvariant_tensorProduct_of_flat A
    (AdicCompletion 𝔭 A) B G
  obtain ⟨x, hx⟩ := Algebra.IsInvariant.isInvariant
    (A := AdicCompletion 𝔭 A) (B := (AdicCompletion 𝔭 A) ⊗[A] B) (G := G) z' hz'fix
  refine ⟨x, ?_⟩

  have hbc : completionBaseChangeHom B 𝔭 x = w := by
    rw [completionBaseChangeHom_eq_tensor, show (x ⊗ₜ[A] (1 : B)) = z' from hx,
      show tensorRingHom B 𝔭 z' = w from (tensorRingEquiv B 𝔭).apply_symm_apply w]
  show semilocalComponent _ (mem_index_self A B G 𝔭 𝔓).2 (completionBaseChangeHom B 𝔭 x) = y
  rw [hbc, hwF ⟨𝔓, mem_index_self A B G 𝔭 𝔓⟩]
  exact (transportOf_eq_of_fixed A B G (gO ⟨𝔓, mem_index_self A B G 𝔭 𝔓⟩) 1
    (hgO ⟨𝔓, mem_index_self A B G 𝔭 𝔓⟩).symm (one_smul G 𝔓) y hy).trans
    (transportOf_one A B G 𝔓 y)

noncomputable def invariantsCompletionEquiv :
    letI := stabilizerMulSemiringAction A B G 𝔓
    haveI := stabilizer_smulCommClass A B G 𝔓
    AdicCompletion 𝔭 A ≃ₐ[A]
      FixedPoints.subalgebra A (AdicCompletion 𝔓 B) (MulAction.stabilizer G 𝔓) := by
  letI := stabilizerMulSemiringAction A B G 𝔓
  haveI := stabilizer_smulCommClass A B G 𝔓
  refine AlgEquiv.ofBijective
    ((invariantsCompletionHom A B G 𝔭 𝔓).codRestrict
      (FixedPoints.subalgebra A (AdicCompletion 𝔓 B) (MulAction.stabilizer G 𝔓))
      fun x h => stabAut_invariantsCompletionHom A B G 𝔭 𝔓 h x) ⟨?_, ?_⟩
  · intro x y hxy
    exact invariantsCompletionHom_injective A B G 𝔭 𝔓 (congrArg Subtype.val hxy)
  · rintro ⟨y, hy⟩
    obtain ⟨x, hx⟩ := exists_invariantsCompletionHom_eq A B G 𝔭 𝔓 y hy
    exact ⟨x, Subtype.ext hx⟩

include G in

noncomputable def invariantsCompletionRingEquiv :
    letI := stabilizerMulSemiringAction A B G 𝔓
    haveI := stabilizer_smulCommClass A B G 𝔓
    AdicCompletion 𝔭 A ≃+*
      FixedPoints.subalgebra A (AdicCompletion 𝔓 B) (MulAction.stabilizer G 𝔓) :=
  (invariantsCompletionEquiv A B G 𝔭 𝔓).toRingEquiv

include G in
omit [Finite G] [IsNoetherianRing A] [Module.Finite A B] [FaithfulSMul A B]
  [Algebra.IsInvariant A B G] [𝔓.IsPrime] in

theorem mem_fixedPoints_iff (x : AdicCompletion 𝔓 B) :
    (letI := stabilizerMulSemiringAction A B G 𝔓
    haveI := stabilizer_smulCommClass A B G 𝔓
    x ∈ FixedPoints.subalgebra A (AdicCompletion 𝔓 B) (MulAction.stabilizer G 𝔓)) ↔
      ∀ h : MulAction.stabilizer G 𝔓, stabAut A B G 𝔓 h x = x :=
  Iff.rfl

end AdicCompletion

end SameUniverseHead

set_option pp.universes true in
#check @AdicCompletion.transportOf
set_option pp.universes true in
#check @AdicCompletion.transportOf_eq_of_fixed
#print axioms AdicCompletion.liesOver_of_isPrime_of_map_le
#print axioms AdicCompletion.isMaximal_of_isPrime_of_liesOver
#print axioms AdicCompletion.isMaximal_and_map_le_iff
#print axioms AdicCompletion.exists_smul_eq_of_liesOver
#print axioms AdicCompletion.map_toAlgEquiv_le_of_smul_le
#print axioms AdicCompletion.transportOf
#print axioms AdicCompletion.evalₐ_transportOf
#print axioms AdicCompletion.transportOf_of
#print axioms AdicCompletion.transportOf_eq_of_fixed
#print axioms AdicCompletion.map_algebraMap_le_smul
#print axioms AdicCompletion.semilocalComponent_selfSmul

set_option pp.universes true in
#check @AdicCompletion.invariantsCompletionEquiv
set_option pp.universes true in
#check @AdicCompletion.invariantsCompletionHom
#print axioms AdicCompletion.isNoetherianRing_of_finite_algebra
#print axioms AdicCompletion.isArtinianRing_quotient_map
#print axioms AdicCompletion.mem_index_self
#print axioms AdicCompletion.smul_mem_index
#print axioms AdicCompletion.completionBaseChangeHom_eq_tensor
#print axioms AdicCompletion.completionBaseChangeHom_injective
#print axioms AdicCompletion.invariantsCompletionHom
#print axioms AdicCompletion.evalₐ_invariantsCompletionHom
#print axioms AdicCompletion.stabAut_invariantsCompletionHom
#print axioms AdicCompletion.eq_of_component_eq_of_smul_eq
#print axioms AdicCompletion.transportOf_one
#print axioms AdicCompletion.evalₐ_component_selfSmul
#print axioms AdicCompletion.evalₐ_component
#print axioms AdicCompletion.invariantsCompletionHom_injective
#print axioms AdicCompletion.exists_invariantsCompletionHom_eq
#print axioms AdicCompletion.invariantsCompletionEquiv
#print axioms AdicCompletion.invariantsCompletionRingEquiv
#print axioms AdicCompletion.mem_fixedPoints_iff