Base change distributes over biproducts

Base change along a morphism of commutative monoid objects sends the biproduct of two modules to the biproduct of their base changes, as bundled modules over the new base. The forward map projects componentwise; the inverse injects componentwise; both are linear over the new base, and they are mutually inverse.

theorem RS.modBiprodInl_fst {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modBiprodInl A M N) (modBiprodFst A M N) = CategoryTheory.CategoryStruct.id M

The first injection followed by the first projection is the identity, at the level of module morphisms.

theorem RS.modBiprodInr_snd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modBiprodInr A M N) (modBiprodSnd A M N) = CategoryTheory.CategoryStruct.id N

The second injection followed by the second projection is the identity, at the level of module morphisms.

noncomputable def RS.baseChangeBiprodFwd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (M N : CategoryTheory.Mod D A) : baseChange φ (modBiprod A M N) ⟶ baseChange φ M ⊞ baseChange φ N

The forward map: the base change of a biproduct projects componentwise onto the biproduct of the base changes.

Equations

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

noncomputable def RS.baseChangeBiprodBwd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (M N : CategoryTheory.Mod D A) : baseChange φ M ⊞ baseChange φ N ⟶ baseChange φ (modBiprod A M N)

The backward map: the biproduct of the base changes injects componentwise into the base change of the biproduct.

Equations

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

theorem RS.baseChangeBiprodBwd_fwd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (baseChangeBiprodBwd A B φ M N) (baseChangeBiprodFwd A B φ M N) = CategoryTheory.CategoryStruct.id (baseChange φ M ⊞ baseChange φ N)

The backward map followed by the forward map is the identity.

theorem RS.baseChangeBiprodFwd_bwd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (baseChangeBiprodFwd A B φ M N) (baseChangeBiprodBwd A B φ M N) = CategoryTheory.CategoryStruct.id (baseChange φ (modBiprod A M N))

The forward map followed by the backward map is the identity.

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

Base change of a module morphism is linear over the new base.

theorem RS.baseChangeAct_baseChangeBiprodFwd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (baseChangeAct φ (modBiprod A M N)) (baseChangeBiprodFwd A B φ M N) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (baseChangeBiprodFwd A B φ M N)) (modBiprodAct B (baseChangeMod φ M) (baseChangeMod φ N))

The forward map intertwines the actions.

theorem RS.modBiprodAct_baseChangeBiprodBwd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modBiprodAct B (baseChangeMod φ M) (baseChangeMod φ N)) (baseChangeBiprodBwd A B φ M N) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (baseChangeBiprodBwd A B φ M N)) (baseChangeAct φ (modBiprod A M N))

The backward map intertwines the actions.

noncomputable def RS.baseChangeBiprodIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (M N : CategoryTheory.Mod D A) : baseChangeMod φ (modBiprod A M N) ≅ modBiprod B (baseChangeMod φ M) (baseChangeMod φ N)

Base change distributes over the biproduct: the base change of a biproduct of modules is the biproduct of the base changes, as bundled modules over the new base.

Equations

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