Complete splitting under field isomorphisms #
Complete splitting depends on the extension, not on its presentation as a field carrier. Transporting the upstairs field over the downstairs field identifies the fibres of place restriction and preserves the extension degree. This allows a compositum to be placed in a finite Galois overfield without changing its splitting behaviour.
theorem
TauCeti.Place.isSplitCompletely_iff_of_algEquiv
{k : Type u_1}
{F : Type u_2}
{L : Type u_3}
{L' : Type u_4}
[Field k]
[Field F]
[Field L]
[Field L']
[Algebra k F]
[Algebra k L]
[Algebra k L']
[Algebra F L]
[Algebra F L']
[IsScalarTower k F L]
[IsScalarTower k F L']
[Algebra.IsIntegral F L]
[Algebra.IsIntegral F L']
(P : Place k F)
(e : L ≃ₐ[F] L')
:
Complete splitting is invariant under an isomorphism of the upstairs field over the base field.