Galois Compatible Fiber Product

Abstract

Compatible Galois restrictions reconstruct the generated compositum.

Theorem 1.1 (The compositum Galois group is the compatible fiber product).

$$\mathrm{Gal}(L,K)\sim \mathrm{FiberProduct}(\mathrm{Gal}(LLeft,K),\mathrm{Gal}(LRight,K),\mathrm{Gal}(\mathrm{Intersection}(LLeft,LRight),K)).$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/GaloisCompatibleFiberProduct.galois_compatible_fiber_product (✓ std3). ∎

Source. Repository-derived.

Commentary.

The ambient field is generated by the two finite subextensions. Restriction identifies its automorphism group with pairs agreeing on their named sharedField.

Injectivity uses the fixing subgroup of the supremum. For surjectivity, the proof changes base to the intersection, where Mathlib’s trivial-intersection lifting theorem applies.

The right extension only needs normality; separability on that side was removed by the assumption audit. The Lean edge-case audit covers trivial maps, equal fields, containment, and failure of ambient generation.

References

• Truth anchor: D5/S3/Factorization/Galois/GaloisCompatibleFiberProduct.galois_compatible_fiber_product
• Dependency: D5/S3/Factorization/Galois/GaloisFusion