Images of idempotent affine-group endomorphisms

The image of an idempotent endomorphism is its fixed subgroup, scheme-theoretically: the coordinate image factorization splits, and its points over every commutative test algebra are exactly the fixed points. In particular this applies to regular Jordan projections of commutative affine groups.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §§15–16.

@[simp]

theorem TauCeti.CommHopfAlgCat.imageι_comp_mkImage_of_idempotent {k : Type u} [Field k] {H : CommHopfAlgCat k} (f : H ⟶ H) (hf : CategoryTheory.CategoryStruct.comp f f = f) : CategoryTheory.CategoryStruct.comp (imageι f) (mkImage f) = CategoryTheory.CategoryStruct.id (image f)

The coordinate image factorization of an idempotent endomorphism is a retraction.

@[simp]

theorem TauCeti.CommHopfAlgCat.mem_quotientPointsSubgroup_ker_iff_mapDomain_eq_self {k : Type u} [Field k] {H : CommHopfAlgCat k} (f : H ⟶ H) (hf : CategoryTheory.CategoryStruct.comp f f = f) (A : CommAlgCat k) (g : WithConv (↑H →ₐ[k] ↑A)) : g ∈ quotientPointsSubgroup H (HopfIdeal.ker (CommHopfAlgCat.Hom.hom f)) A ↔ (CommHopfAlgCat.Hom.hom f).mapDomain g = g

The image of an idempotent affine-group endomorphism represents its fixed points over all commutative test algebras, including nonreduced algebras.