Base change of a free module

Base change along a morphism of commutative monoid objects sends the free module on an object to the free module over the new base: B ⊗[A] (A ⊗ V) ≅ B ⊗ V as B-modules.

• baseChangeFreeHom/baseChangeFreeInv: the two carrier maps, descending multiplication through φ and inserting the unit of A respectively.
• baseChangeFreeIso: the isomorphism baseChangeMod φ (freeMod A V) ≅ freeMod B V in the category of B-modules.

theorem RS.pushMul_pushMul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B φ) CategoryTheory.MonObj.mul) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B φ) CategoryTheory.MonObj.mul) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B A A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul φ)) CategoryTheory.MonObj.mul)

Multiplying through φ twice is multiplying through φ once after multiplying in A.

theorem RS.mul_pushMul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A B : D) [CategoryTheory.MonObj B] (φ : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B φ) CategoryTheory.MonObj.mul) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B B A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B φ) CategoryTheory.MonObj.mul)) CategoryTheory.MonObj.mul)

Multiplying in B before pushing through φ is multiplying in B after.

theorem RS.legM_restrictRegular_freeMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (V : D) : modTensorLegM A (restrictRegular φ) (freeMod A V) = CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B φ) CategoryTheory.MonObj.mul) (CategoryTheory.MonoidalCategoryStruct.tensorObj A V)

The first module-tensor leg of the base change of a free module, at carrier atoms.

theorem RS.baseChangeFree_condition_atoms {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (V : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B φ) CategoryTheory.MonObj.mul) (CategoryTheory.MonoidalCategoryStruct.tensorObj A V)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B A V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B φ) CategoryTheory.MonObj.mul) V)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B A (CategoryTheory.MonoidalCategoryStruct.tensorObj A V)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V)))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B A V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B φ) CategoryTheory.MonObj.mul) V))

The comparison map coequalizes the two module-tensor legs, stated at carrier atoms.

theorem RS.baseChangeFree_condition {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (V : D) : CategoryTheory.CategoryStruct.comp (modTensorLegM A (restrictRegular φ) (freeMod A V)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B A V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B φ) CategoryTheory.MonObj.mul) V)) = CategoryTheory.CategoryStruct.comp (modTensorLegN A (restrictRegular φ) (freeMod A V)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B A V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B φ) CategoryTheory.MonObj.mul) V))

The comparison map coequalizes the two module-tensor legs.

noncomputable def RS.baseChangeFreeHom {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 φ] (V : D) : baseChange φ (freeMod A V) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj B V

The comparison map from the base change of a free module to the free module over the new base.

Equations

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

theorem RS.modTensorπ_baseChangeFreeHom {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 φ] (V : D) : CategoryTheory.CategoryStruct.comp (modTensorπ A (restrictRegular φ) (freeMod A V)) (baseChangeFreeHom A B φ V) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B A V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B φ) CategoryTheory.MonObj.mul) V)

Defining equation of the comparison map.

theorem RS.modTensorπ_baseChangeFreeHom_assoc {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 φ] (V : D) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj B V ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (modTensorπ A (restrictRegular φ) (freeMod A V)) (baseChangeFreeHom A B φ V)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B A V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B φ) CategoryTheory.MonObj.mul) V)) h

Defining equation of the comparison map.

noncomputable def RS.baseChangeFreeInv {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] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (V : D) : CategoryTheory.MonoidalCategoryStruct.tensorObj B V ⟶ baseChange φ (freeMod A V)

The inverse comparison map: insert the unit of A.

Equations

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

theorem RS.baseChangeFree_balance {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 φ] (V : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B φ) CategoryTheory.MonObj.mul) (CategoryTheory.MonoidalCategoryStruct.tensorObj A V)) (modTensorπ A (restrictRegular φ) (freeMod A V)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B A (CategoryTheory.MonoidalCategoryStruct.tensorObj A V)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V)))) (modTensorπ A (restrictRegular φ) (freeMod A V))

The balance relation of the base-change projection on a free module, at carrier atoms.

theorem RS.baseChangeFree_balance_assoc {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 φ] (V : D) {Z : D} (h : modTensor A (restrictRegular φ) (freeMod A V) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B φ) CategoryTheory.MonObj.mul) (CategoryTheory.MonoidalCategoryStruct.tensorObj A V)) (modTensorπ A (restrictRegular φ) (freeMod A V))) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B A (CategoryTheory.MonoidalCategoryStruct.tensorObj A V)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V)))) (modTensorπ A (restrictRegular φ) (freeMod A V))) h

The balance relation of the base-change projection on a free module, at carrier atoms.

theorem RS.baseChangeFree_retract {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 φ] (V : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B A V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B φ) CategoryTheory.MonObj.mul) V)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one V))) (modTensorπ A (restrictRegular φ) (freeMod A V))) = modTensorπ A (restrictRegular φ) (freeMod A V)

Multiplying out and reinserting the unit of A returns the projection: the retract identity behind hom ≫ inv = 𝟙.

theorem RS.baseChangeFree_hom_inv {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 φ] (V : D) : CategoryTheory.CategoryStruct.comp (baseChangeFreeHom A B φ V) (baseChangeFreeInv A B φ V) = CategoryTheory.CategoryStruct.id (baseChange φ (freeMod A V))

The two comparison maps compose to the identity of the base change.

theorem RS.baseChangeFree_section_atoms {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (V : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one V))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B A V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B φ) CategoryTheory.MonObj.mul) V)) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj B V)

Inserting the unit of A and multiplying out through φ is the identity of B ⊗ V.

theorem RS.baseChangeFree_inv_hom {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 φ] (V : D) : CategoryTheory.CategoryStruct.comp (baseChangeFreeInv A B φ V) (baseChangeFreeHom A B φ V) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj B V)

The two comparison maps compose to the identity of the free module over the new base.

theorem RS.baseChangeFree_linear_atoms {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A B : D) [CategoryTheory.MonObj B] (φ : A ⟶ B) (V : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B B (CategoryTheory.MonoidalCategoryStruct.tensorObj A V)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (CategoryTheory.MonoidalCategoryStruct.tensorObj A V))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B A V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B φ) CategoryTheory.MonObj.mul) V)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B A V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B φ) CategoryTheory.MonObj.mul) V))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B B V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V))

The comparison map intertwines the two B-actions, at carrier atoms.

theorem RS.whiskerLeft_π_baseChangeAct_free {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)] (V : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (modTensorπ A (restrictRegular φ) (freeMod A V))) (baseChangeAct φ (freeMod A V)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B B (CategoryTheory.MonoidalCategoryStruct.tensorObj A V)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (CategoryTheory.MonoidalCategoryStruct.tensorObj A V))) (modTensorπ A (restrictRegular φ) (freeMod A V))

Defining equation of the B-action on the base change of a free module, at carrier atoms.

theorem RS.baseChangeAct_baseChangeFreeHom {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)] (V : D) : CategoryTheory.CategoryStruct.comp (baseChangeAct φ (freeMod A V)) (baseChangeFreeHom A B φ V) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (baseChangeFreeHom A B φ V)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B B V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V))

The comparison map is B-linear.

theorem RS.baseChangeAct_baseChangeFreeHom_assoc {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)] (V : D) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj B V ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeAct φ (freeMod A V)) (CategoryTheory.CategoryStruct.comp (baseChangeFreeHom A B φ V) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (baseChangeFreeHom A B φ V)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B B V).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V) h))

The comparison map is B-linear.

theorem RS.freeAct_baseChangeFreeInv {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)] (V : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B B V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V)) (baseChangeFreeInv A B φ V) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (baseChangeFreeInv A B φ V)) (baseChangeAct φ (freeMod A V))

The inverse comparison map is B-linear.

noncomputable def RS.baseChangeFreeIso {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)] (V : D) : baseChangeMod φ (freeMod A V) ≅ freeMod B V

Base change of a free module: the base change along φ of the free A-module on V is the free B-module on V, as an isomorphism of B-modules.

Equations

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