FiniteInvariantRingImage.lean

theorem eval₂_eq_zero_of_lift_and_fixed_coefficients
    {A C T : Type*} [CommRing A] [CommRing C] [CommRing T]
    (a : A →+* C) (f : C →+* T) (σ : T →+* T)
    (hσ : σ.comp (f.comp a) = f.comp a)
    (p : Polynomial A) (q : Polynomial C) (hp : p.map a = q)
    (x : C) (hx : q.eval x = 0) :
    q.eval₂ f (σ.toFun (f.toFun x)) = 0

theorem exists_smul_of_eval₂_charpoly_eq_zero
    {C T H : Type*} [CommRing C] [CommRing T] [IsDomain T]
    [Group H] [Fintype H] [MulSemiringAction H C]
    (f : C →+* T) (x : C) (y : T)
    (hy : (MulSemiringAction.charpoly H x).eval₂ f y = 0) :
    ∃ h : H, y = f.toFun (h • x)

theorem exists_smul_ringHom_apply_of_invariant
    {A C T H : Type*} [CommRing A] [CommRing C] [CommRing T] [IsDomain T]
    [Algebra A C] [Group H] [Finite H] [MulSemiringAction H C]
    [Algebra.IsInvariant A C H]
    (f : C →+* T) (φ : T ≃+* T)
    (hφ : φ.toRingHom.comp (f.comp (algebraMap A C)) =
      f.comp (algebraMap A C))
    (x : C) :
    ∃ h : H, φ.toRingHom.toFun (f.toFun x) = f.toFun (h • x)