The quotient-branch element calculation

This file formalizes the remaining element calculation in the first Pogorzały--Skowroński kernel obstruction. In the source notation, X = L / rad³ L, the second radical layer is the direct sum S ⊕ T, and Y = X/S, Z = X/T. A vector outside both branch radicals lifts to a generator of X. Sending that generator to a vector with one nonzero component in each of S and T produces the mixed socle vector; vanishing of the third radical layer makes the two branch actions agree.

theorem MagnitudeConjecture.RightModule.quotientBranch_hasMixedSocleSmulWitness {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (X : FinitelyGeneratedCategory A) (S T : Submodule Aᵐᵒᵖ ↑X) (hinf : S ⊓ T = ⊥) (hSsimple : IsSimpleModule Aᵐᵒᵖ ↥S) (hTsimple : IsSimpleModule Aᵐᵒᵖ ↥T) (hSTrad : S ⊔ T ≤ Module.jacobson Aᵐᵒᵖ ↑X) (hXtop : IsSimpleModule Aᵐᵒᵖ ↑(quotientFGObj X (Module.jacobson Aᵐᵒᵖ ↑X))) (hradicalSquare : Ring.jacobson Aᵐᵒᵖ ^ 2 • ⊤ = S ⊔ T) (hradicalCube : Ring.jacobson Aᵐᵒᵖ ^ 3 • ⊤ = ⊥) (hYuniserial : IsUniserialModule Aᵐᵒᵖ ↑(quotientFGObj X S)) (hZuniserial : IsUniserialModule Aᵐᵒᵖ ↑(quotientFGObj X T)) (P : Submodule Aᵐᵒᵖ ↑(quotientBranchFiberKernelFGObj X S T (Module.jacobson Aᵐᵒᵖ ↑X) hSTrad)) (houtside : ¬P ≤ quotientBranchFiberKernelRadicalPreimage X S T (Module.jacobson Aᵐᵒᵖ ↑X) hSTrad) : HasMixedSocleSmulWitness (quotientFGObj X S) (quotientFGObj X T) (quotientFGObj X (Module.jacobson Aᵐᵒᵖ ↑X)) (quotientFGMapQ X S (Module.jacobson Aᵐᵒᵖ ↑X) ⋯) (quotientFGMapQ X T (Module.jacobson Aᵐᵒᵖ ↑X) ⋯) P