Magnitude conjecture

MagnitudeConjecture.Algebra.BiserialRadicalSquareTruncation

Radical-square truncations in the biserial induction #

The second Pogorzały--Skowroński reduction replaces a local module L by L / rad² L. This file packages that literal quotient and the canonical identification of its radical with rad L / rad² L.

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

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

Instances For
    source
    def MagnitudeConjecture.RightModule.radicalSquareTruncationFGObj {A : Type u} [Ring A] (L : FinitelyGeneratedCategory A) :
    FinitelyGeneratedCategory A

    The literal radical-square truncation L / rad² L.

    Instances For
      source
      def MagnitudeConjecture.RightModule.radicalSquareTruncationMkQ {A : Type u} [Ring A] (L : FinitelyGeneratedCategory A) :
      ↑L →ₗ[Aᵐᵒᵖ] ↑(radicalSquareTruncationFGObj L)

      The quotient map to L / rad² L.

      Instances For
        source
        @[simp]
        theorem MagnitudeConjecture.RightModule.radicalSquareTruncationMkQ_apply {A : Type u} [Ring A] (L : FinitelyGeneratedCategory A) (x : ↑L) :
        (radicalSquareTruncationMkQ L) x = (radicalSquareSubmodule L).mkQ x
        source
        theorem MagnitudeConjecture.RightModule.ringJacobson_square_smul_top_radicalSquareTruncation_eq_bot {A : Type u} [Ring A] (L : FinitelyGeneratedCategory A) :
        Ring.jacobson Aᵐᵒᵖ ^ 2 • ⊤ = ⊥

        The square of the ring radical annihilates L / rad² L.

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

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

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

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

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

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

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

          Radical-square truncation preserves simplicity of the module top.

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

          The canonical embedding of rad L / rad² L into L / rad² L.

          Instances For
            source
            theorem MagnitudeConjecture.RightModule.radicalTopToSquareTruncationMap_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (L : FinitelyGeneratedCategory A) :
            Function.Injective ⇑(radicalTopToSquareTruncationMap L)

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

            source
            theorem MagnitudeConjecture.RightModule.radicalTopToSquareTruncationMap_range {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (L : FinitelyGeneratedCategory A) :
            (radicalTopToSquareTruncationMap L).range = Module.jacobson Aᵐᵒᵖ ↑(radicalSquareTruncationFGObj L)

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

            source
            theorem MagnitudeConjecture.RightModule.moduleJacobson_jacobson_radicalSquareTruncation_eq_bot {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (L : FinitelyGeneratedCategory A) :
            Module.jacobson Aᵐᵒᵖ ↥(Module.jacobson Aᵐᵒᵖ ↑(radicalSquareTruncationFGObj L)) = ⊥

            The first radical of L / rad² L has zero module radical.

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

            The radical top of L is canonically the radical top of L / rad² L.

            Instances For