Transport of a splitting along a base change

The base-change comparison of free modules is natural in the object, so a section of a free morphism over one algebra base-changes to a section over any algebra under it.

theorem RS.baseChangeFreeInv_natural {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} (f : V ⟶ W) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B f) (baseChangeFreeInv A B φ W) = CategoryTheory.CategoryStruct.comp (baseChangeFreeInv A B φ V) (baseChangeMapMod A B φ (freeModMap A f)).hom

The base-change comparison is natural, at the carrier.

theorem RS.baseChangeFreeIso_inv_natural {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} (f : V ⟶ W) : CategoryTheory.CategoryStruct.comp (freeModMap B f) (baseChangeFreeIso A B φ W).inv = CategoryTheory.CategoryStruct.comp (baseChangeFreeIso A B φ V).inv (baseChangeMapMod A B φ (freeModMap A f))

The base-change comparison is natural, as module maps.

theorem RS.exists_section_baseChange {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} (g : V ⟶ W) (s : freeMod A W ⟶ freeMod A V) (hs : CategoryTheory.CategoryStruct.comp s (freeModMap A g) = CategoryTheory.CategoryStruct.id (freeMod A W)) : ∃ (t : freeMod B W ⟶ freeMod B V), CategoryTheory.CategoryStruct.comp t (freeModMap B g) = CategoryTheory.CategoryStruct.id (freeMod B W)

A section of a free morphism base-changes.