Magnitude conjecture

MagnitudeConjecture.Algebra.BiserialFiberKernelElementCapture

Element capture in a biserial fiber kernel #

The element calculation in the first Pogorzały--Skowroński obstruction produces a vector with two nonzero socle coordinates inside a hypothetical uniserial summand, while that summand already contains one coordinate socle. The lemmas below prove that these data force the summand to contain the whole fiber-kernel socle.

source
def MagnitudeConjecture.RightModule.fiberKernelLeftSocleMap {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z Top : FinitelyGeneratedCategory A) (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑Top) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑Top) (hYkill : moduleSocle Aᵐᵒᵖ ↑Y ≤ f.ker) :
↥(moduleSocle Aᵐᵒᵖ ↑Y) →ₗ[Aᵐᵒᵖ] ↑(fiberKernelFGObj Y Z Top f g)

Embed the left branch socle as the left coordinate of the fiber kernel.

Instances For
    source
    def MagnitudeConjecture.RightModule.fiberKernelRightSocleMap {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z Top : FinitelyGeneratedCategory A) (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑Top) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑Top) (hZkill : moduleSocle Aᵐᵒᵖ ↑Z ≤ g.ker) :
    ↥(moduleSocle Aᵐᵒᵖ ↑Z) →ₗ[Aᵐᵒᵖ] ↑(fiberKernelFGObj Y Z Top f g)

    Embed the right branch socle as the right coordinate of the fiber kernel.

    Instances For
      source
      @[simp]
      theorem MagnitudeConjecture.RightModule.fiberKernelInclusion_leftSocleMap {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z Top : FinitelyGeneratedCategory A) (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑Top) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑Top) (hYkill : moduleSocle Aᵐᵒᵖ ↑Y ≤ f.ker) (y : ↥(moduleSocle Aᵐᵒᵖ ↑Y)) :
      (fiberKernelInclusion Y Z Top f g) ((fiberKernelLeftSocleMap Y Z Top f g hYkill) y) = (↑y, 0)

      The ambient inclusion sends the left socle embedding to (y,0).

      source
      @[simp]
      theorem MagnitudeConjecture.RightModule.fiberKernelInclusion_rightSocleMap {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z Top : FinitelyGeneratedCategory A) (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑Top) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑Top) (hZkill : moduleSocle Aᵐᵒᵖ ↑Z ≤ g.ker) (z : ↥(moduleSocle Aᵐᵒᵖ ↑Z)) :
      (fiberKernelInclusion Y Z Top f g) ((fiberKernelRightSocleMap Y Z Top f g hZkill) z) = (0, ↑z)

      The ambient inclusion sends the right socle embedding to (0,z).

      source
      theorem MagnitudeConjecture.RightModule.fiberKernelLeftSocleMap_injective {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z Top : FinitelyGeneratedCategory A) (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑Top) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑Top) (hYkill : moduleSocle Aᵐᵒᵖ ↑Y ≤ f.ker) :
      Function.Injective ⇑(fiberKernelLeftSocleMap Y Z Top f g hYkill)

      The left socle embedding is injective.

      source
      theorem MagnitudeConjecture.RightModule.fiberKernelRightSocleMap_injective {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z Top : FinitelyGeneratedCategory A) (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑Top) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑Top) (hZkill : moduleSocle Aᵐᵒᵖ ↑Z ≤ g.ker) :
      Function.Injective ⇑(fiberKernelRightSocleMap Y Z Top f g hZkill)

      The right socle embedding is injective.

      source
      def MagnitudeConjecture.RightModule.fiberKernelLeftSocleSubmodule {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z Top : FinitelyGeneratedCategory A) (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑Top) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑Top) (hYkill : moduleSocle Aᵐᵒᵖ ↑Y ≤ f.ker) :
      Submodule Aᵐᵒᵖ ↑(fiberKernelFGObj Y Z Top f g)

      The left coordinate copy of the branch socle in the fiber kernel.

      Instances For
        source
        def MagnitudeConjecture.RightModule.fiberKernelRightSocleSubmodule {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z Top : FinitelyGeneratedCategory A) (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑Top) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑Top) (hZkill : moduleSocle Aᵐᵒᵖ ↑Z ≤ g.ker) :
        Submodule Aᵐᵒᵖ ↑(fiberKernelFGObj Y Z Top f g)

        The right coordinate copy of the branch socle in the fiber kernel.

        Instances For
          source
          def MagnitudeConjecture.RightModule.HasMixedSocleCoordinates {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z Top : FinitelyGeneratedCategory A) (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑Top) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑Top) (P : Submodule Aᵐᵒᵖ ↑(fiberKernelFGObj Y Z Top f g)) :
          Prop

          A submodule of a fiber kernel contains a vector with two nonzero branch socle coordinates.

          Instances For
            source
            def MagnitudeConjecture.RightModule.HasMixedSocleSmulWitness {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z Top : FinitelyGeneratedCategory A) (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑Top) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑Top) (P : Submodule Aᵐᵒᵖ ↑(fiberKernelFGObj Y Z Top f g)) :
            Prop

            A source-shaped witness for mixed socle coordinates: one scalar sends the two coordinates of a vector in P to nonzero elements of the corresponding branch socles.

            Instances For
              source
              theorem MagnitudeConjecture.RightModule.hasMixedSocleCoordinates_of_smulWitness {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z Top : FinitelyGeneratedCategory A) (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑Top) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑Top) (P : Submodule Aᵐᵒᵖ ↑(fiberKernelFGObj Y Z Top f g)) (h : HasMixedSocleSmulWitness Y Z Top f g P) :
              HasMixedSocleCoordinates Y Z Top f g P

              A scalar-action witness produces a vector with mixed nonzero socle coordinates.

              source
              theorem MagnitudeConjecture.RightModule.hasMixedSocleSmulWitness_of_length_three {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z Top : FinitelyGeneratedCategory A) (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑Top) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑Top) (hYsimple : IsSimpleModule Aᵐᵒᵖ ↥(moduleSocle Aᵐᵒᵖ ↑Y)) (hZsimple : IsSimpleModule Aᵐᵒᵖ ↥(moduleSocle Aᵐᵒᵖ ↑Z)) (hYkill : moduleSocle Aᵐᵒᵖ ↑Y ≤ f.ker) (hZkill : moduleSocle Aᵐᵒᵖ ↑Z ≤ g.ker) [IsArtinian Aᵐᵒᵖ ↑(fiberKernelFGObj Y Z Top f g)] (P : Submodule Aᵐᵒᵖ ↑(fiberKernelFGObj Y Z Top f g)) (hPne : P ≠ ⊥) (hPuniserial : IsUniserialModule Aᵐᵒᵖ ↥P) (hPlength : Module.length Aᵐᵒᵖ ↥P = 3) (u : ↥P) (hu : u ∉ Module.jacobson Aᵐᵒᵖ ↥P) (hnonzero : ∀ r ∈ Ring.jacobson Aᵐᵒᵖ ^ 2, r • u ≠ 0 → r • ((fiberKernelInclusion Y Z Top f g) ↑u).1 ≠ 0 ∧ r • ((fiberKernelInclusion Y Z Top f g) ↑u).2 ≠ 0) :
              HasMixedSocleSmulWitness Y Z Top f g P

              The radical-square calculation for a length-three uniserial submodule produces a source-shaped mixed-socle witness as soon as nonvanishing of the two ambient coordinates is known. Membership of those coordinates in the branch socles is automatic: the submodule socle maps into the fiber-kernel socle, and the latter maps onto the product of the branch socles.

              source
              theorem MagnitudeConjecture.RightModule.moduleSocle_fiberKernel_le_of_coordinateSocles_le {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z Top : FinitelyGeneratedCategory A) (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑Top) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑Top) (hYsimple : IsSimpleModule Aᵐᵒᵖ ↥(moduleSocle Aᵐᵒᵖ ↑Y)) (hZsimple : IsSimpleModule Aᵐᵒᵖ ↥(moduleSocle Aᵐᵒᵖ ↑Z)) (hYkill : moduleSocle Aᵐᵒᵖ ↑Y ≤ f.ker) (hZkill : moduleSocle Aᵐᵒᵖ ↑Z ≤ g.ker) (P : Submodule Aᵐᵒᵖ ↑(fiberKernelFGObj Y Z Top f g)) (hleft : fiberKernelLeftSocleSubmodule Y Z Top f g hYkill ≤ P) (hright : fiberKernelRightSocleSubmodule Y Z Top f g hZkill ≤ P) :
              moduleSocle Aᵐᵒᵖ ↑(fiberKernelFGObj Y Z Top f g) ≤ P

              A submodule containing both coordinate socles contains the entire socle of the fiber kernel.

              source
              theorem MagnitudeConjecture.RightModule.fiberKernel_coordinateSocle_le_of_simpleSocle {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z Top : FinitelyGeneratedCategory A) (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑Top) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑Top) (hYsimple : IsSimpleModule Aᵐᵒᵖ ↥(moduleSocle Aᵐᵒᵖ ↑Y)) (hZsimple : IsSimpleModule Aᵐᵒᵖ ↥(moduleSocle Aᵐᵒᵖ ↑Z)) (hnoniso : ¬Nonempty (↥(moduleSocle Aᵐᵒᵖ ↑Y) ≃ₗ[Aᵐᵒᵖ] ↥(moduleSocle Aᵐᵒᵖ ↑Z))) (hYkill : moduleSocle Aᵐᵒᵖ ↑Y ≤ f.ker) (hZkill : moduleSocle Aᵐᵒᵖ ↑Z ≤ g.ker) [IsArtinian Aᵐᵒᵖ ↑(fiberKernelFGObj Y Z Top f g)] (P : Submodule Aᵐᵒᵖ ↑(fiberKernelFGObj Y Z Top f g)) (hPsocleSimple : IsSimpleModule Aᵐᵒᵖ ↥(moduleSocle Aᵐᵒᵖ ↥P)) :
              fiberKernelLeftSocleSubmodule Y Z Top f g hYkill ≤ P ∨ fiberKernelRightSocleSubmodule Y Z Top f g hZkill ≤ P

              If the two simple branch socles are non-isomorphic, every nonzero submodule with simple intrinsic socle contains one of their coordinate copies.

              source
              theorem MagnitudeConjecture.RightModule.moduleSocle_fiberKernel_le_of_mixed_of_coordinate_le {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z Top : FinitelyGeneratedCategory A) (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑Top) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑Top) (hYsimple : IsSimpleModule Aᵐᵒᵖ ↥(moduleSocle Aᵐᵒᵖ ↑Y)) (hZsimple : IsSimpleModule Aᵐᵒᵖ ↥(moduleSocle Aᵐᵒᵖ ↑Z)) (hYkill : moduleSocle Aᵐᵒᵖ ↑Y ≤ f.ker) (hZkill : moduleSocle Aᵐᵒᵖ ↑Z ≤ g.ker) (P : Submodule Aᵐᵒᵖ ↑(fiberKernelFGObj Y Z Top f g)) (y : ↥(moduleSocle Aᵐᵒᵖ ↑Y)) (z : ↥(moduleSocle Aᵐᵒᵖ ↑Z)) (hy : y ≠ 0) (hz : z ≠ 0) (hmixed : (fiberKernelLeftSocleMap Y Z Top f g hYkill) y + (fiberKernelRightSocleMap Y Z Top f g hZkill) z ∈ P) (hside : fiberKernelLeftSocleSubmodule Y Z Top f g hYkill ≤ P ∨ fiberKernelRightSocleSubmodule Y Z Top f g hZkill ≤ P) :
              moduleSocle Aᵐᵒᵖ ↑(fiberKernelFGObj Y Z Top f g) ≤ P

              A submodule containing one coordinate socle and one vector whose two socle coordinates are nonzero contains the whole fiber-kernel socle.

              source
              theorem MagnitudeConjecture.RightModule.moduleSocle_fiberKernel_le_of_mixed_of_nonisomorphic {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z Top : FinitelyGeneratedCategory A) (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑Top) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑Top) (hYsimple : IsSimpleModule Aᵐᵒᵖ ↥(moduleSocle Aᵐᵒᵖ ↑Y)) (hZsimple : IsSimpleModule Aᵐᵒᵖ ↥(moduleSocle Aᵐᵒᵖ ↑Z)) (hnoniso : ¬Nonempty (↥(moduleSocle Aᵐᵒᵖ ↑Y) ≃ₗ[Aᵐᵒᵖ] ↥(moduleSocle Aᵐᵒᵖ ↑Z))) (hYkill : moduleSocle Aᵐᵒᵖ ↑Y ≤ f.ker) (hZkill : moduleSocle Aᵐᵒᵖ ↑Z ≤ g.ker) [IsArtinian Aᵐᵒᵖ ↑(fiberKernelFGObj Y Z Top f g)] (P : Submodule Aᵐᵒᵖ ↑(fiberKernelFGObj Y Z Top f g)) (hPsocleSimple : IsSimpleModule Aᵐᵒᵖ ↥(moduleSocle Aᵐᵒᵖ ↥P)) (y : ↥(moduleSocle Aᵐᵒᵖ ↑Y)) (z : ↥(moduleSocle Aᵐᵒᵖ ↑Z)) (hy : y ≠ 0) (hz : z ≠ 0) (hmixed : (fiberKernelLeftSocleMap Y Z Top f g hYkill) y + (fiberKernelRightSocleMap Y Z Top f g hZkill) z ∈ P) :
              moduleSocle Aᵐᵒᵖ ↑(fiberKernelFGObj Y Z Top f g) ≤ P

              For non-isomorphic simple branch socles, a mixed vector with two nonzero socle coordinates already forces a nonzero submodule with simple socle to contain the whole fiber-kernel socle.

              source
              theorem MagnitudeConjecture.RightModule.moduleSocle_fiberKernel_le_of_hasMixed_of_nonisomorphic {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (Y Z Top : FinitelyGeneratedCategory A) (f : ↑Y →ₗ[Aᵐᵒᵖ] ↑Top) (g : ↑Z →ₗ[Aᵐᵒᵖ] ↑Top) (hYsimple : IsSimpleModule Aᵐᵒᵖ ↥(moduleSocle Aᵐᵒᵖ ↑Y)) (hZsimple : IsSimpleModule Aᵐᵒᵖ ↥(moduleSocle Aᵐᵒᵖ ↑Z)) (hnoniso : ¬Nonempty (↥(moduleSocle Aᵐᵒᵖ ↑Y) ≃ₗ[Aᵐᵒᵖ] ↥(moduleSocle Aᵐᵒᵖ ↑Z))) (hYkill : moduleSocle Aᵐᵒᵖ ↑Y ≤ f.ker) (hZkill : moduleSocle Aᵐᵒᵖ ↑Z ≤ g.ker) [IsArtinian Aᵐᵒᵖ ↑(fiberKernelFGObj Y Z Top f g)] (P : Submodule Aᵐᵒᵖ ↑(fiberKernelFGObj Y Z Top f g)) (hPsocleSimple : IsSimpleModule Aᵐᵒᵖ ↥(moduleSocle Aᵐᵒᵖ ↥P)) (hmixed : HasMixedSocleCoordinates Y Z Top f g P) :
              moduleSocle Aᵐᵒᵖ ↑(fiberKernelFGObj Y Z Top f g) ≤ P

              The coordinate-free mixed-vector predicate supplies the concrete sum of the two coordinate socle embeddings used by the capture theorem.