Kernel subquotient obstructions for biseriality

The Pogorzały--Skowroński induction repeatedly constructs a kernel inside a binary product and exhibits two equal composition layers in it. This file packages the routine module-theoretic part: a product of two branch submodules, modulo branch submodules with a common quotient, is a repeated self-subquotient of the kernel.

theorem MagnitudeConjecture.RightModule.hasRepeatedSelfSubquotient_of_prod_submodule_quotients {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z F : FinitelyGeneratedCategory A) [Nontrivial ↑F] (W : Submodule Aᵐᵒᵖ ↑(prodFGObj Y Z)) (PY : Submodule Aᵐᵒᵖ ↑Y) (PZ : Submodule Aᵐᵒᵖ ↑Z) (hPW : PY.prod PZ ≤ W) (QY : Submodule Aᵐᵒᵖ ↥PY) (QZ : Submodule Aᵐᵒᵖ ↥PZ) (eY : (↥PY ⧸ QY) ≃ₗ[Aᵐᵒᵖ] ↑F) (eZ : (↥PZ ⧸ QZ) ≃ₗ[Aᵐᵒᵖ] ↑F) : HasRepeatedSelfSubquotient (submoduleFGObj (prodFGObj Y Z) W)

A product of two submodules with the same nonzero quotient gives a repeated self-subquotient of every ambient submodule which contains that product.

theorem MagnitudeConjecture.RightModule.hasRepeatedSelfSubquotient_kernel_of_prod_submodule_quotients {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z T F : FinitelyGeneratedCategory A) [Nontrivial ↑F] (g : ↑Y × ↑Z →ₗ[Aᵐᵒᵖ] ↑T) (PY : Submodule Aᵐᵒᵖ ↑Y) (PZ : Submodule Aᵐᵒᵖ ↑Z) (hkill : ∀ (y : ↥PY) (z : ↥PZ), g (↑y, ↑z) = 0) (QY : Submodule Aᵐᵒᵖ ↥PY) (QZ : Submodule Aᵐᵒᵖ ↥PZ) (eY : (↥PY ⧸ QY) ≃ₗ[Aᵐᵒᵖ] ↑F) (eZ : (↥PZ ⧸ QZ) ≃ₗ[Aᵐᵒᵖ] ↑F) : HasRepeatedSelfSubquotient (submoduleFGObj (prodFGObj Y Z) g.ker)

Kernel form of the product-subquotient obstruction. It is enough to check that the branch product is killed by the defining map.

def MagnitudeConjecture.RightModule.fiberKernelMap {A : Type u} [Ring A] (Y Z T : FinitelyGeneratedCategory A) (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑T) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑T) : ↑Y × ↑Z →ₗ[Aᵐᵒᵖ] ↑T

Difference of two maps to a common target. Its kernel is their module fiber product.

def MagnitudeConjecture.RightModule.fiberKernelFGObj {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z T : FinitelyGeneratedCategory A) (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑T) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑T) : FinitelyGeneratedCategory A

The finitely generated module carried by a module fiber product.

theorem MagnitudeConjecture.RightModule.hasRepeatedSelfSubquotient_fiberKernel_of_submodule_quotients {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z T F : FinitelyGeneratedCategory A) [Nontrivial ↑F] (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑T) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑T) (PY : Submodule Aᵐᵒᵖ ↑Y) (PZ : Submodule Aᵐᵒᵖ ↑Z) (hPY : PY ≤ f.ker) (hPZ : PZ ≤ g.ker) (QY : Submodule Aᵐᵒᵖ ↥PY) (QZ : Submodule Aᵐᵒᵖ ↥PZ) (eY : (↥PY ⧸ QY) ≃ₗ[Aᵐᵒᵖ] ↑F) (eZ : (↥PZ ⧸ QZ) ≃ₗ[Aᵐᵒᵖ] ↑F) : HasRepeatedSelfSubquotient (fiberKernelFGObj Y Z T f g)

If both branch maps kill submodules with the same nonzero quotient, their fiber-product kernel has a repeated self-subquotient.

theorem MagnitudeConjecture.RightModule.not_indec_fiberKernel_of_all_coordinateThin {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {ι : Type w} [Fintype ι] (e : ι → A) (hall : CompleteOrthogonalIdempotents e) (H : AllIndecomposablesCoordinateThin e) (Y Z T F : FinitelyGeneratedCategory A) [Nontrivial ↑F] (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑T) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑T) (PY : Submodule Aᵐᵒᵖ ↑Y) (PZ : Submodule Aᵐᵒᵖ ↑Z) (hPY : PY ≤ f.ker) (hPZ : PZ ≤ g.ker) (QY : Submodule Aᵐᵒᵖ ↥PY) (QZ : Submodule Aᵐᵒᵖ ↥PZ) (eY : (↥PY ⧸ QY) ≃ₗ[Aᵐᵒᵖ] ↑F) (eZ : (↥PZ ⧸ QZ) ≃ₗ[Aᵐᵒᵖ] ↑F) : ¬CategoryTheory.Indecomposable (fiberKernelFGObj Y Z T f g)

Under complete coordinate thinness, a fiber-product kernel carrying the two equal branch quotients above cannot be indecomposable. This is the exact contradiction endpoint for the kernel modules in the Pogorzały--Skowroński induction.