feat(FieldTheory/Galois/IsGaloisGroup): add version of IsGaloisGroup.to_isFractionRing assuming only IsIntegral (leanprover-community#39091)

This PR adds a version of `IsGaloisGroup.to_isFractionRing` assuming only `Algebra.IsIntegral A B` (which is weaker than the existing assumption `Finite G`).

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

@@ -132,13 +132,20 @@ variable (G A B K L : Type*) [Group G] [CommRing A] [CommRing B] [MulSemiringAct
   [MulSemiringAction G L] [SMulDistribClass G B L]
 
 /-- `IsGaloisGroup` for rings implies `IsGaloisGroup` for their fraction fields. -/
-theorem IsGaloisGroup.to_isFractionRing [Finite G] [hGAB : IsGaloisGroup G A B] :
+theorem IsGaloisGroup.to_isFractionRing_of_isIntegral
+    [Algebra.IsIntegral A B] [hGAB : IsGaloisGroup G A B] :
     IsGaloisGroup G K L where
   faithful :=
     have := hGAB.faithful
     IsFractionRing.faithfulSMul G B L
   commutes := IsFractionRing.smulCommClass G A B K L
-  isInvariant := IsFractionRing.isInvariant G A B K L
+  isInvariant := IsFractionRing.isInvariant_of_isIntegral G A B K L
+
+/-- `IsGaloisGroup` for rings implies `IsGaloisGroup` for their fraction fields. -/
+theorem IsGaloisGroup.to_isFractionRing [Finite G] [hGAB : IsGaloisGroup G A B] :
+    IsGaloisGroup G K L :=
+  have := hGAB.isInvariant.isIntegral
+  IsGaloisGroup.to_isFractionRing_of_isIntegral G A B K L
 
 /-- If `B` is an integral extension of an integrally closed domain `A`, then `IsGaloisGroup` for
 their fraction fields implies `IsGaloisGroup` for these rings. -/

Mathlib/RingTheory/Invariant/Basic.lean

@@ -532,18 +532,17 @@ end normal
 
 namespace IsFractionRing
 
+variable (G A B K L : Type*) [Group G] [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L]
+  [Algebra K L] [Algebra A K] [Algebra B L] [Algebra A L] [IsFractionRing A K] [IsFractionRing B L]
+  [IsScalarTower A K L] [IsScalarTower A B L] [MulSemiringAction G B] [MulSemiringAction G L]
+  [SMulDistribClass G B L] [hAB : Algebra.IsInvariant A B G] [SMulCommClass G A B]
+
 /-- If `G` acts on `B/A` with `A` as the fixed subring, then `G` also acts on `L/K` with `K` as
 the fixed subfield, where `K` and `L` are the fraction fields of `A` and `B` respectively. -/
-theorem isInvariant (G A B K L : Type*) [Group G] [CommRing A] [CommRing B] [MulSemiringAction G B]
-    [Algebra A B] [Field K] [Field L] [Algebra K L] [Algebra A K] [Algebra B L] [Algebra A L]
-    [IsFractionRing A K] [IsFractionRing B L] [IsScalarTower A K L] [IsScalarTower A B L]
-    [MulSemiringAction G L] [SMulDistribClass G B L] [Finite G] [hAB : Algebra.IsInvariant A B G]
-    [SMulCommClass G A B] :
-    Algebra.IsInvariant K L G := by
+theorem isInvariant_of_isIntegral [Algebra.IsIntegral A B] : Algebra.IsInvariant K L G := by
   refine ⟨fun x h ↦ ?_⟩
   have hc (a : A) : (algebraMap K L) (algebraMap A K a) = (algebraMap B L) (algebraMap A B a) := by
     simp_rw [← IsScalarTower.algebraMap_apply]
-  have := hAB.isIntegral A B G
   have : Nontrivial A := (IsFractionRing.nontrivial_iff_nontrivial A K).mpr inferInstance
   have : Nontrivial B := (IsFractionRing.nontrivial_iff_nontrivial B L).mpr inferInstance
   obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective B x
@@ -559,4 +558,11 @@ theorem isInvariant (G A B K L : Type*) [Group G] [CommRing A] [CommRing B] [Mul
   use algebraMap A K b / algebraMap A K a
   rw [hxy, map_div₀, hc, hc]
 
+include A B in
+/-- If `G` acts on `B/A` with `A` as the fixed subring, then `G` also acts on `L/K` with `K` as
+the fixed subfield, where `K` and `L` are the fraction fields of `A` and `B` respectively. -/
+theorem isInvariant [Finite G] : Algebra.IsInvariant K L G :=
+  have := hAB.isIntegral
+  isInvariant_of_isIntegral G A B K L
+
 end IsFractionRing