feat(IsGaloisGroup): if B/A and B/A' are Galois with the same Galois group, then A ≃+* A' (leanprover-community#35797)

Author: xroblot

Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

@@ -42,7 +42,7 @@ open Module
 
 section CommRing
 
-variable (G A B : Type*) [Group G] [CommSemiring A] [Semiring B] [Algebra A B]
+variable (G A A' B : Type*) [Group G] [CommSemiring A] [Semiring B] [Algebra A B]
   [MulSemiringAction G B]
 
 /-- `G` is a Galois group for `L/K` if the action of `G` on `L` is faithful with fixed field `K`.
@@ -67,6 +67,46 @@ theorem IsGaloisGroup.of_mulEquiv [hG : IsGaloisGroup G A B] {H : Type*} [Group
 
 attribute [instance low] IsGaloisGroup.commutes IsGaloisGroup.isInvariant
 
+variable [FaithfulSMul A B] [hA : IsGaloisGroup G A B]
+
+/--
+If `B/A` is Galois with Galois group `G`, then `A` is isomorphic to the subring of elements of `B`
+fixed by `G`.
+-/
+@[simps apply_coe]
+noncomputable def IsGaloisGroup.ringEquivFixedPoints :
+    A ≃+* FixedPoints.subsemiring B G where
+  toFun x := ⟨algebraMap A B x, fun _ ↦ by rw [smul_algebraMap]⟩
+  invFun x := (hA.isInvariant.isInvariant x x.prop).choose
+  map_mul' _ _ := by simp [Subtype.ext_iff]
+  map_add' _ _ := by simp [Subtype.ext_iff]
+  left_inv _ := by simp
+  right_inv x := by simpa [Subtype.ext_iff] using (hA.isInvariant.isInvariant x x.prop).choose_spec
+
+@[simp]
+theorem IsGaloisGroup.algebraMap_ringEquivFixedPoints_symm_apply (x : FixedPoints.subsemiring B G) :
+    algebraMap A B ((ringEquivFixedPoints G A B).symm x) = x :=
+ (hA.isInvariant.isInvariant x x.prop).choose_spec
+
+variable [CommSemiring A'] [Algebra A' B] [FaithfulSMul A' B] [hA' : IsGaloisGroup G A' B]
+
+/--
+If `B/A` and `B/A'` are Galois with the same Galois group, then `A ≃+* A'`.
+-/
+noncomputable def IsGaloisGroup.ringEquiv :
+    A ≃+* A' :=
+  (ringEquivFixedPoints G A B).trans (ringEquivFixedPoints G A' B).symm
+
+@[simp]
+theorem IsGaloisGroup.algebraMap_ringEquiv_apply (x : A) :
+    algebraMap A' B (IsGaloisGroup.ringEquiv G A A' B x) = algebraMap A B x := by
+  simp [ringEquiv]
+
+@[simp]
+theorem IsGaloisGroup.algebraMap_ringEquiv_symm_apply (x : A') :
+    algebraMap A B ((IsGaloisGroup.ringEquiv G A A' B).symm x) = algebraMap A' B x := by
+  simp [ringEquiv]
+
 end CommRing
 
 section Field