Transport of the dévissage decomposition

The decomposition of a state is carried along a base change and recombined with the splitting of the remainder: one further unit summand joins the mixed free part.

noncomputable def RS.baseChangeMapMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] {P Q : CategoryTheory.Mod D A} (g : P ⟶ Q) : baseChangeMod φ P ⟶ baseChangeMod φ Q

Base change on morphisms of modules.

Equations

• RS.baseChangeMapMod A B φ g = CategoryTheory.Mod.Hom.mk' (RS.modTensorMap A (CategoryTheory.CategoryStruct.id (RS.restrictRegular φ)) g) ⋯

@[simp]

theorem RS.baseChangeMapMod_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] {P Q : CategoryTheory.Mod D A} (g : P ⟶ Q) : (baseChangeMapMod A B φ g).hom = modTensorMap A (CategoryTheory.CategoryStruct.id (restrictRegular φ)) g

noncomputable def RS.baseChangeMapIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] {P Q : CategoryTheory.Mod D A} (e : P ≅ Q) : baseChangeMod φ P ≅ baseChangeMod φ Q

Base change is functorial on isomorphisms.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.freeMixSuccIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (B : D) [CategoryTheory.MonObj B] (L : OddLine D) (r s : ℕ) : modBiprod B (regularMod B) (freeMod B (L.mix r s)) ≅ freeMod B (L.mix (r + 1) s)

The mixed free part absorbs a unit summand.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.transportDecomp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (L : OddLine D) (r s : ℕ) {X : D} {R : CategoryTheory.Mod D A} (e : freeMod A X ≅ modBiprod A (freeMod A (L.mix r s)) R) {R'' : CategoryTheory.Mod D B} (f : baseChangeMod φ R ≅ modBiprod B (regularMod B) R'') : freeMod B X ≅ modBiprod B (freeMod B (L.mix (r + 1) s)) R''

The transported decomposition: a state decomposition, base-changed and recombined with a splitting of the remainder, gains one unit summand in the mixed free part.

Equations

• One or more equations did not get rendered due to their size.