Galois Fusion

Abstract

Galois restrictions fuse through their common intersection field.

Theorem 1.1 (Joint restrictions satisfy the shared-field constraint).

$$\mathrm{JointRestriction}(sigma)\in \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/GaloisFusion.joint_restriction_lands_in_fiber_product (✓ std3). ∎

Source. Repository-derived.

Commentary.

The named sharedField is the intersection of the two observer fields. Restricting either component again to this field gives the same automorphism, so every joint output belongs to the named groupFiberProduct.

This compatibility needs normality of both subextensions so the restriction homomorphisms exist. It does not need finiteness, generation of the ambient field, or trivial intersection.

Theorem 1.2 (Finite Galois disjointness is trivial intersection).

$$\mathrm{LinearDisjoint}(LLeft,LRight)⟺\mathrm{Intersection}(LLeft,LRight)=K.$$

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

Source. Repository-derived.

Commentary.

This is a thin wrapper around Mathlib’s exact theorem. Its asymmetric hypotheses require the left extension to be Galois and both extensions to be finite dimensional.

Theorem 1.3 (Trivial intersection gives the Galois product).

$$\begin{gathered} \mathrm{Intersection}(LLeft,LRight)=K\Rightarrow \\ \mathrm{Gal}(L,K)\sim \mathrm{Gal}(LLeft,K)\times \mathrm{Gal}(LRight,K). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

When the two finite Galois subfields generate the ambient field and meet only in the base, joint restriction is bijective. The resulting multiplicative equivalence is exactly the joint restriction homomorphism.

Surjectivity uses Mathlib’s linear-disjoint restriction lifting. Injectivity uses the fixing subgroup of a supremum. No general Galois theory is reproved.

Lemma 1.4 (Different names do not imply independent observations).

$$\mathrm{SharedField}(C,C)\ne R\wedge \neg \mathrm{Surjective}(\mathrm{Diagonal}(\mathrm{Gal}(C,R))).$$

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

Source. Repository-derived.

Commentary.

Name the same nontrivial extension C over R twice. Their intersection is nontrivial, and the joint observation is diagonal. It cannot reach the pair consisting of identity and complex conjugation.

Lemma 1.5 (The ambient field must be generated by the observer fields).

$$\mathrm{Intersection}(R,R)=R\wedge \neg \mathrm{Injective}(\mathrm{JointRestriction}(\mathrm{Gal}(C,R))).$$

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

Source. Repository-derived.

Commentary.

Inside C over R, take both observer fields to be the base field. Their intersection is trivial, but identity and complex conjugation have the same two restrictions. This is the concrete audit for the supremum-equals-top hypothesis.

Theorem 1.6 (The unramified Frobenius output restricts compatibly).

$$\begin{gathered} \mathrm{Unramified}(Q)\Rightarrow \\ \mathrm{RestrictionPair}(\mathrm{Frob}(Q))\in \mathrm{FiberProduct}(GalLeft,GalRight,\mathrm{SharedGaloisGroup}(LLeft,LRight)). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

The proof reuses mathlibFrobeniusAt. On the unramified branch it maps its chosen arithmetic Frobenius conjugacy class through each Galois restriction homomorphism.

The resulting representative pair belongs to groupFiberProduct as a conclusion. Abelianity is not used: conjugacy classes make the statement valid for the stronger nonabelian setting.

Pinned Mathlib has no naturality theorem equating these images with separately chosen arithFrobAt values on intermediate rings.

Lemma 1.7 (The ramified branch has no Frobenius class).

$$\mathrm{Ramified}(Q)\Rightarrow \mathrm{mathlibFrobeniusAt}(Q)=none.$$

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

Source. Repository-derived.

Commentary.

Unfolding the existing observer shows that any ramified ideal is tagged none. Thus the unramified premise is genuinely used by the some-valued Frobenius fusion conclusion.

Lemma 1.8 (A concrete cyclotomic field has a ramified prime).

$$\exists P\in \mathrm{MaxSpec}(\mathrm{RingOfIntegers}(\mathrm{CyclotomicField}(3,\mathbb{Q}))),\mathrm{RamifiedOver}(P,\mathbb{Z}).$$

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

Source. Repository-derived.

Commentary.

The third cyclotomic field has degree two over Q. Mathlib’s number-field ramification theorem therefore supplies a maximal ideal of its ring of integers that is ramified over Z.

The Lean audits also cover empty carriers, restriction to the base, equal observer fields, and the completely trivial extension. There is no numeric depth parameter to test at zero.

References

• Truth anchor: D5/S3/Factorization/Galois/GaloisFusion.composite_generation_is_necessary
• Truth anchor: D5/S3/Factorization/Galois/GaloisFusion.differently_named_extensions_not_independent
• Truth anchor: D5/S3/Factorization/Galois/GaloisFusion.frobenius_fusion_compatible
• Truth anchor: D5/S3/Factorization/Galois/GaloisFusion.joint_restriction_lands_in_fiber_product
• Truth anchor: D5/S3/Factorization/Galois/GaloisFusion.linearDisjoint_iff_trivial_intersection
• Truth anchor: D5/S3/Factorization/Galois/GaloisFusion.ramification_hypothesis_is_necessary
• Truth anchor: D5/S3/Factorization/Galois/GaloisFusion.ramified_frobenius_is_none
• Truth anchor: D5/S3/Factorization/Galois/GaloisFusion.trivial_intersection_galois_product
• Dependency: D5/S3/Factorization/Galois/GaloisPrimeObserver