English
Base change commutes with finite products: for a finite index set ι, the family of maps given by f i preserves base-change under the pi-construction.
Русский
Изменение базы сохраняется при конечных производных: для конечного набора индексов ι семейство отображений сохраняет изменение базы при глобальном произведении по индексам.
LaTeX
$$$IsBaseChange\\; S\\; (\\pi f)$$$
Lean4
/-- Base change commutes with finite products. -/
theorem pi {ι : Type*} [Finite ι] {M M' : ι → Type*} [∀ i, AddCommMonoid (M i)] [∀ i, AddCommMonoid (M' i)]
[∀ i, Module R (M i)] [∀ i, Module R (M' i)] [∀ i, Module S (M' i)] [∀ i, IsScalarTower R S (M' i)]
(f : ∀ i, M i →ₗ[R] M' i) (hf : ∀ i, IsBaseChange S (f i)) : IsBaseChange S (.pi fun i ↦ f i ∘ₗ .proj i) := by
classical
cases nonempty_fintype ι
apply of_equiv <| TensorProduct.piRight R S _ M ≪≫ₗ .piCongrRight fun i ↦ (hf i).equiv
intro x
ext i
simp [equiv_tmul]
