English
Base change along S for f and base change along T for h are equivalent to base change for the composed map.
Русский
Базовое изменение вдоль S для f и базовое изменение вдоль T для h эквивалентны базовому изменению для композиции h ∘ f.
LaTeX
$$$ IsBaseChange S f \to IsBaseChange T h \;\Longleftrightarrow\; IsBaseChange T (h \circ f)$$$
Lean4
theorem comp {f : M →ₗ[R] N} (hf : IsBaseChange S f) {g : N →ₗ[S] O} (hg : IsBaseChange T g) :
IsBaseChange T ((g.restrictScalars R).comp f) :=
by
apply IsBaseChange.of_lift_unique
intro Q _ _ _ _ i
letI := Module.compHom Q (algebraMap S T)
haveI : IsScalarTower S T Q :=
⟨fun x y z => by
rw [Algebra.smul_def, mul_smul]
rfl⟩
have : IsScalarTower R S Q := by
refine ⟨fun x y z => ?_⟩
change (IsScalarTower.toAlgHom R S T) (x • y) • z = x • algebraMap S T y • z
rw [map_smul, smul_assoc]
rfl
refine
⟨hg.lift (hf.lift i), by
ext
simp [IsBaseChange.lift_eq], ?_⟩
rintro g' (e : _ = _)
refine hg.algHom_ext' _ _ (hf.algHom_ext' _ _ ?_)
rw [IsBaseChange.lift_comp, IsBaseChange.lift_comp, ← e]
ext
rfl
