Fixed point of algebra equiv is the field itself.

Stream: new members

[Junjie Bai]

I want to show that the fixed points of a AlgEquiv (L [M] L) is just M. But I don't know how to show that two fixed field of two subgroup is equal if the two subgroup is equvalance. Here is a #mwe :

import Mathlib

variable {M L : Type*} [Field M] [Field L] [Algebra M L] [Normal M L] [Algebra.IsSeparable M L]

open IntermediateField

example : fixedField (⊤ : Subgroup (L ≃ₐ[M] L)) = fixedField (fixingSubgroup (⊥ : IntermediateField M L)) := by sorry

Or it's there any better way to solve this problem?

[Kevin Buzzard]

simp solves this. And this makes sense: statements like docs#IntermediateField.fixingSubgroup_bot are very natural simp lemmas because the RHS is unambiguously simpler than the LHS.

[Junjie Bai]

Thanks a lot! It seems that the version I'm using is too old so I can't find it :sleeping: