Transport of local mixedness along a base change #
Being a mixed sum after base change is inherited by any further base change: the free module on an object is carried to the free module on the same object, so a decomposition over one algebra becomes a decomposition over any algebra under it.
noncomputable def
RS.freeModIsoBaseChange
{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 φ]
{V W : D}
(e : freeMod A V ≅ freeMod A W)
:
An isomorphism of free modules base-changes.
Equations
- RS.freeModIsoBaseChange A B φ e = (RS.baseChangeFreeIso A B φ V).symm ≪≫ RS.baseChangeMapIso A B φ e ≪≫ RS.baseChangeFreeIso A B φ W