Ring of invariants via typeclass system

Stream: Is there code for X?

[Kevin Buzzard]

I have a commutative ring R, an R-algebra A and a (finite) group G acting on A. I would like to express the fact that the image of R in A is precisely the G-invariants of A. This implies SMulCommClass G R A but it is strictly stronger; SMulCommClass just means (after a little calculation) that the image of R in A is a subset of the G-invariants.

I don't want to restrict to R : Subring A because in the applications I'll have things like R=\R and A=\C and G being {1,complex conjugation}.

Ideally I would do this entirely within the typeclass framework. Right now I'm carrying around the clunky

variable (hGalois : ∀ (b : B), (∀ (g : G), g • b = b) ↔ ∃ a : A, b = a)

(sorry, B was an A-algebra there)

[Daniel Weber]

You can say that docs#MulAction.fixedPoints is equal to the range of algebraMap R A, but I'm not sure if that's better than what you currently have

[Antoine Chambert-Loir]

Define the sub algebra RG of G-invariants and prove that algebraMap A R induces an isomorphism from A to RG?

[Filippo A. E. Nuccio]

Have you tried to set up a docs#GaloisInsertion between subgroups of Gand sub-R-algebras of A and then use Algebra.coe_bot ? Along the lines of docs#LieSubalgebra.gi