Radical-cube truncations in the biserial induction

The first Pogorzały--Skowroński obstruction replaces a local module L by the literal quotient X = L / rad³ L. This file packages that quotient and proves the three structural facts used downstream: the third ring-radical layer vanishes, the second layer is its image from L, and the simple top is unchanged.

theorem MagnitudeConjecture.map_ideal_smul_top_quotient {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (I : Ideal R) (K : Submodule R M) : Submodule.map K.mkQ (I • ⊤) = I • ⊤

An ideal-generated layer commutes with a module quotient.

theorem MagnitudeConjecture.ideal_smul_top_quotient_eq_bot_of_le {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (I : Ideal R) (K : Submodule R M) (hIK : I • ⊤ ≤ K) : I • ⊤ = ⊥

Quotienting by a submodule containing an ideal-generated layer kills that layer.

theorem MagnitudeConjecture.isSimpleModule_of_map_of_injective {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Injective ⇑f) (P : Submodule R M) (hP : IsSimpleModule R ↥(Submodule.map f P)) : IsSimpleModule R ↥P

If an injective linear map sends a submodule to a simple module, then the original submodule is simple.

noncomputable def MagnitudeConjecture.submoduleMapLinearEquivOfInjective {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Injective ⇑f) (P : Submodule R M) : ↥P ≃ₗ[R] ↥(Submodule.map f P)

An injective linear map identifies a submodule with its image.

noncomputable def MagnitudeConjecture.submoduleQuotientLinearEquivMap {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (P Q : Submodule R M) : (↥P ⧸ Submodule.comap P.subtype Q) ≃ₗ[R] ↥(Submodule.map Q.mkQ P)

The quotient of one submodule by its intersection with another is the image of the first submodule in the ambient quotient by the second.

noncomputable def MagnitudeConjecture.submoduleLinearEquivMapQuotientOfInfEqBot {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (P Q : Submodule R M) (hinf : P ⊓ Q = ⊥) : ↥P ≃ₗ[R] ↥(Submodule.map Q.mkQ P)

A submodule disjoint from the quotient denominator is canonically equivalent to its image in the quotient.

noncomputable def MagnitudeConjecture.moduleTopOfMappedSubmoduleQuotientLinearEquiv {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (P Q : Submodule R M) (hQrad : Submodule.comap P.subtype Q ≤ Module.jacobson R ↥P) : (↥(Submodule.map Q.mkQ P) ⧸ Module.jacobson R ↥(Submodule.map Q.mkQ P)) ≃ₗ[R] ↥P ⧸ Module.jacobson R ↥P

Quotienting an ambient module by Q and then taking the top of the image of P does not change the top of P, provided the part of Q lying in P is radical.

noncomputable def MagnitudeConjecture.submoduleProdSupLinearEquiv {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (P Q : Submodule R M) (hinf : P ⊓ Q = ⊥) : (↥P × ↥Q) ≃ₗ[R] ↥(P ⊔ Q)

Two disjoint submodules identify their product with their sum.

theorem MagnitudeConjecture.length_sup_eq_two_of_disjoint_simple {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (P Q : Submodule R M) (hinf : P ⊓ Q = ⊥) (hP : IsSimpleModule R ↥P) (hQ : IsSimpleModule R ↥Q) : Module.length R ↥(P ⊔ Q) = 2

The sum of two disjoint simple submodules has composition length two.

theorem MagnitudeConjecture.length_eq_four_of_three_simple_radical_layers {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] (S T : Submodule R M) (hinf : S ⊓ T = ⊥) (hS : IsSimpleModule R ↥S) (hT : IsSimpleModule R ↥T) (hSTJ : S ⊔ T ≤ Module.jacobson R M) (hJquot : IsSimpleModule R (↥(Module.jacobson R M) ⧸ Submodule.comap (Module.jacobson R M).subtype (S ⊔ T))) (htop : IsSimpleModule R (M ⧸ Module.jacobson R M)) : Module.length R M = 4

A module with one simple top layer, one simple middle radical layer, and a bottom layer that is the sum of two disjoint simples has composition length four.

def MagnitudeConjecture.RightModule.radicalCubeSubmodule {A : Type u} [Ring A] (L : FinitelyGeneratedCategory A) : Submodule Aᵐᵒᵖ ↑L

The third ring-radical layer of a finitely generated right module.

def MagnitudeConjecture.RightModule.radicalCubeTruncationFGObj {A : Type u} [Ring A] (L : FinitelyGeneratedCategory A) : FinitelyGeneratedCategory A

The literal radical-cube truncation L / rad³ L used in the Pogorzały--Skowroński induction.

def MagnitudeConjecture.RightModule.radicalCubeTruncationMkQ {A : Type u} [Ring A] (L : FinitelyGeneratedCategory A) : ↑L →ₗ[Aᵐᵒᵖ] ↑(radicalCubeTruncationFGObj L)

The quotient map to the radical-cube truncation.

@[simp]

theorem MagnitudeConjecture.RightModule.radicalCubeTruncationMkQ_apply {A : Type u} [Ring A] (L : FinitelyGeneratedCategory A) (x : ↑L) : (radicalCubeTruncationMkQ L) x = (radicalCubeSubmodule L).mkQ x

theorem MagnitudeConjecture.RightModule.ringJacobson_cube_smul_top_radicalCubeTruncation_eq_bot {A : Type u} [Ring A] (L : FinitelyGeneratedCategory A) : Ring.jacobson Aᵐᵒᵖ ^ 3 • ⊤ = ⊥

The third ring-radical layer vanishes in L / rad³ L.

theorem MagnitudeConjecture.RightModule.map_ringJacobson_square_smul_top_radicalCubeTruncation {A : Type u} [Ring A] (L : FinitelyGeneratedCategory A) : Submodule.map (radicalCubeTruncationMkQ L) (Ring.jacobson Aᵐᵒᵖ ^ 2 • ⊤) = Ring.jacobson Aᵐᵒᵖ ^ 2 • ⊤

The second ring-radical layer of L / rad³ L is exactly the image of the second layer of L.

noncomputable def MagnitudeConjecture.RightModule.radicalSecondTopToCubeTruncationMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (L : FinitelyGeneratedCategory A) : ↥(Module.jacobson Aᵐᵒᵖ ↥(Module.jacobson Aᵐᵒᵖ ↑L)) ⧸ Module.jacobson Aᵐᵒᵖ ↥(Module.jacobson Aᵐᵒᵖ ↥(Module.jacobson Aᵐᵒᵖ ↑L)) →ₗ[Aᵐᵒᵖ] ↑(radicalCubeTruncationFGObj L)

The canonical embedding of rad² L / rad³ L into the literal radical-cube truncation L / rad³ L.

theorem MagnitudeConjecture.RightModule.radicalSecondTopToCubeTruncationMap_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (L : FinitelyGeneratedCategory A) : Function.Injective ⇑(radicalSecondTopToCubeTruncationMap L)

The map from rad² L / rad³ L into L / rad³ L is injective.

theorem MagnitudeConjecture.RightModule.radicalSecondTopToCubeTruncationMap_range {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (L : FinitelyGeneratedCategory A) : (radicalSecondTopToCubeTruncationMap L).range = Ring.jacobson Aᵐᵒᵖ ^ 2 • ⊤

The image of rad² L / rad³ L is exactly the second radical layer of L / rad³ L.

theorem MagnitudeConjecture.RightModule.moduleJacobson_radicalCubeTruncation_eq_map {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (L : FinitelyGeneratedCategory A) : Module.jacobson Aᵐᵒᵖ ↑(radicalCubeTruncationFGObj L) = Submodule.map (radicalCubeTruncationMkQ L) (Module.jacobson Aᵐᵒᵖ ↑L)

The radical of L / rad³ L is the image of the radical of L.

theorem MagnitudeConjecture.RightModule.radicalCubeSubmodule_le_moduleJacobson {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (L : FinitelyGeneratedCategory A) : radicalCubeSubmodule L ≤ Module.jacobson Aᵐᵒᵖ ↑L

The third radical layer of L lies in its first radical.

def MagnitudeConjecture.RightModule.radicalCubeTruncationTopLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (L : FinitelyGeneratedCategory A) : ↑(quotientFGObj (radicalCubeTruncationFGObj L) (Module.jacobson Aᵐᵒᵖ ↑(radicalCubeTruncationFGObj L))) ≃ₗ[Aᵐᵒᵖ] ↑(quotientFGObj L (Module.jacobson Aᵐᵒᵖ ↑L))

The top of L / rad³ L is canonically the top of L.

theorem MagnitudeConjecture.RightModule.isSimpleModule_top_radicalCubeTruncation_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (L : FinitelyGeneratedCategory A) : IsSimpleModule Aᵐᵒᵖ ↑(quotientFGObj (radicalCubeTruncationFGObj L) (Module.jacobson Aᵐᵒᵖ ↑(radicalCubeTruncationFGObj L))) ↔ IsSimpleModule Aᵐᵒᵖ ↑(quotientFGObj L (Module.jacobson Aᵐᵒᵖ ↑L))

Radical-cube truncation preserves simplicity of the module top.

theorem MagnitudeConjecture.RightModule.isSimpleModule_radicalLayer_radicalCubeTruncation {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (L : FinitelyGeneratedCategory A) (hJtop : IsSimpleModule Aᵐᵒᵖ (↥(Module.jacobson Aᵐᵒᵖ ↑L) ⧸ Module.jacobson Aᵐᵒᵖ ↥(Module.jacobson Aᵐᵒᵖ ↑L))) : IsSimpleModule Aᵐᵒᵖ (↥(Module.jacobson Aᵐᵒᵖ ↑(radicalCubeTruncationFGObj L)) ⧸ Submodule.comap (Module.jacobson Aᵐᵒᵖ ↑(radicalCubeTruncationFGObj L)).subtype (Ring.jacobson Aᵐᵒᵖ ^ 2 • ⊤))

If rad L / rad² L is simple, then it is the simple intervening radical layer inside L / rad³ L.