# Going down for fixed-point subring under finite automorphism group

From Commalg

This fact is an application of the following pivotal fact/result/idea:going up theorem

View other applications of going up theorem OR Read a survey article on applying going up theorem

## Statement

Suppose is a commutative unital ring and is a finite subgroup of the automorphism group of . Suppose is the fixed-point subring. Then, the extension of is a going down extension; in other words, we have *going down* for prime ideals. Explicitly:

If are prime ideals of and is a prime ideal of contracting to then there exists a prime ideal of contracting to , such that .

## Definitions used

*Fill this in later*

## Facts used

- Ring is integral extension of fixed-point subring under finite automorphism group
- Integral extension implies surjective map on spectra
- Automorphism group acts transitively on fibers of spectrum over fixed-point subring
- Going up theorem

## Proof

### Proof outline

- Show that is an integral extension of
- Use the fact that integral extensions give surjective maps on spectra,to find a prime ideal lying over
- Use going up to find a prime ideal lying over and containing
- Use the transitivity of action of on the fiber over to find an automorphism that sends to
- The image of under that automorphism is the required