HenselianInvariantProjection.lean

theorem exists_fixed_mul_eq_of_orthogonal_orbit
    {R : Type v} {G : Type w} [CommRing R] [Group G] [Finite G]
    [MulSemiringAction G R] (e y : R) (hey : e * y = y)
    (hfix : ∀ g : G, g • e = e → g • y = y)
    (horth : ∀ g : G, g • e ≠ e → e * (g • e) = 0) :
    ∃ r : R, (∀ g : G, g • r = r) ∧ e * r = y

theorem algebraMap_away_bijective_of_transitive_completeOrthogonalIdempotents
    (A : Type u) (R : Type v) (G : Type w)
    [CommRing A] [CommRing R] [Algebra A R] [Group G] [Finite G]
    [MulSemiringAction G R] [SMulCommClass G A R] [Algebra.IsInvariant A R G]
    {ι : Type*} [Fintype ι] (σ : G →* Equiv.Perm ι)
    (e : ι → R) (he : CompleteOrthogonalIdempotents e)
    (hσ : ∀ (g : G) (j : ι), g • e j = e (σ g j)) (i : ι)
    (htrans : ∀ j : ι, ∃ g : G, σ g i = j)
    (hinj : Function.Injective (algebraMap A R)) :
    let eH : FixedPoints.subalgebra A R (MulAction.stabilizer G (e i)) :=
      ⟨e i, fun g => g.property⟩
    Function.Bijective (algebraMap A (Localization.Away eH)) := by
  intro eH
  have heH : IsIdempotentElem eH := Subtype.ext (he.idem i).eq
  constructor
  · apply (RingHom.injective_iff_ker_eq_bot (algebraMap A (Localization.Away eH))).mpr
    apply bot_unique
    intro a ha
    change algebraMap A (Localization.Away eH) a = 0 at ha
    change a = 0
    apply hinj
    rw [map_zero]
    have hkill : e i * algebraMap A R a = 0 := by
      have hmap : algebraMap (FixedPoints.subalgebra A R (MulAction.stabilizer G (e i)))
          (Localization.Away eH)
          (algebraMap A (FixedPoints.subalgebra A R (MulAction.stabilizer G (e i))) a) =
        algebraMap (FixedPoints.subalgebra A R (MulAction.stabilizer G (e i)))
          (Localization.Away eH) 0 := by
        rw [← IsScalarTower.algebraMap_apply A
          (FixedPoints.subalgebra A R (MulAction.stabilizer G (e i)))
          (Localization.Away eH), map_zero]
        exact ha
      obtain ⟨⟨_, n, rfl⟩, hs⟩ :=
        (IsLocalization.eq_iff_exists (Submonoid.powers eH) (Localization.Away eH)).mp hmap
      rw [mul_zero] at hs
      have hs' := congrArg
        (fun z : FixedPoints.subalgebra A R (MulAction.stabilizer G (e i)) => eH * z) hs
      rw [mul_zero, ← mul_assoc, ← pow_succ', heH.pow_succ_eq] at hs'
      exact congrArg Subtype.val hs'
    have hall : ∀ j : ι, e j * algebraMap A R a = 0 := by
      intro j
      obtain ⟨g, hg⟩ := htrans j
      have h := congrArg (fun r : R => g • r) hkill
      rw [smul_mul', smul_algebraMap, smul_zero, hσ, hg] at h
      exact h
    have hsum := congrArg (fun r : R => r * algebraMap A R a) he.complete
    rw [Finset.sum_mul, Finset.sum_eq_zero (fun j _ => hall j), one_mul] at hsum
    exact hsum.symm
  · intro z
    obtain ⟨x, rfl⟩ := IsLocalization.Away.algebraMap_surjective_of_isIdempotentElem
      (S := Localization.Away eH) eH heH z
    obtain ⟨r, hr, her⟩ := exists_fixed_mul_eq_of_orthogonal_orbit (e i) (e i * (x : R))
      (by rw [← mul_assoc, (he.idem i).eq])
      (fun (g : G) (hg : g • e i = e i) => by
        have hx : g • (x : R) = (x : R) := x.property ⟨g, hg⟩
        rw [smul_mul', hg, hx]) (by
        intro g hg
        rw [hσ]
        apply he.ortho
        intro hij
        apply hg
        rw [hσ, ← hij])
    obtain ⟨a, ha⟩ := Algebra.IsInvariant.isInvariant (A := A) (G := G) r hr
    refine ⟨a, ?_⟩
    apply (IsLocalization.Away.algebraMap_isUnit
      (S := Localization.Away eH) eH).mul_left_cancel
    rw [IsScalarTower.algebraMap_apply A
      (FixedPoints.subalgebra A R (MulAction.stabilizer G (e i))) (Localization.Away eH),
      ← map_mul, ← map_mul]
    apply congrArg (algebraMap (FixedPoints.subalgebra A R (MulAction.stabilizer G (e i)))
      (Localization.Away eH))
    apply Subtype.ext
    change e i * algebraMap A R a = e i * (x : R)
    rw [ha]
    exact her

theorem span_orbit_eq_top_of_notMem
    (A : Type u) (R : Type v) (G : Type w)
    [CommRing A] [IsLocalRing A] [CommRing R] [Algebra A R]
    [Algebra.IsIntegral A R] [Group G] [Finite G]
    [MulSemiringAction G R] [SMulCommClass G A R] [Algebra.IsInvariant A R G]
    (q : Ideal R) [q.IsPrime] [q.LiesOver (IsLocalRing.maximalIdeal A)]
    (e : R) (heq : e ∉ q) : Ideal.span (MulAction.orbit G e) = ⊤

theorem algebraMap_eq_zero_of_mul_eq_zero_of_notMem
    (A : Type u) (R : Type v) (G : Type w)
    [CommRing A] [IsLocalRing A] [CommRing R] [Algebra A R]
    [Algebra.IsIntegral A R] [Group G] [Finite G]
    [MulSemiringAction G R] [SMulCommClass G A R] [Algebra.IsInvariant A R G]
    (q : Ideal R) [q.IsPrime] [q.LiesOver (IsLocalRing.maximalIdeal A)]
    (e : R) (heq : e ∉ q) (a : A) (hea : e * algebraMap A R a = 0) :
    algebraMap A R a = 0

theorem algebraMap_away_eq_zero_iff_of_notMem
    (A : Type u) (R : Type v) (G : Type w)
    [CommRing A] [IsLocalRing A] [CommRing R] [Algebra A R]
    [Algebra.IsIntegral A R] [Group G] [Finite G]
    [MulSemiringAction G R] [SMulCommClass G A R] [Algebra.IsInvariant A R G]
    (q : Ideal R) [q.IsPrime] [q.LiesOver (IsLocalRing.maximalIdeal A)]
    (e : FixedPoints.subalgebra A R (q.inertia G)) (he : IsIdempotentElem e)
    (heq : (e : R) ∉ q) (a : A) :
    algebraMap A (Localization.Away e) a = 0 ↔ algebraMap A R a = 0

theorem isolatingIdempotent_mul_smul_eq_zero
    (hfinite : ((IsLocalRing.maximalIdeal A).primesOver R).Finite)
    (q : Ideal R) [q.IsPrime] [q.LiesOver (IsLocalRing.maximalIdeal A)]
    (e : R) (he : IsIdempotentElem e)
    (hsupp : ∀ Q : Ideal R, Q.IsPrime → Q.LiesOver (IsLocalRing.maximalIdeal A) →
      (e ∉ Q ↔ Q = q)) (g : G) (hg : g • e ≠ e) : e * (g • e) = 0

theorem exists_base_mul_eq_of_isolatingIdempotent
    [Finite G] [Algebra.IsInvariant A R G]
    [IsSepClosed (IsLocalRing.ResidueField A)]
    (q : Ideal R) [q.IsPrime] [q.LiesOver (IsLocalRing.maximalIdeal A)]
    (e : R) (he : IsIdempotentElem e)
    (hsupp : ∀ Q : Ideal R, Q.IsPrime → Q.LiesOver (IsLocalRing.maximalIdeal A) →
      (e ∉ Q ↔ Q = q))
    (x : FixedPoints.subalgebra A R (q.inertia G)) :
    ∃ a : A, e * algebraMap A R a = e * (x : R)