English
IsBaseChange S f is equivalent to the universal lifting property with respect to all Q; existence and uniqueness of lifts characterize base-change.
Русский
IsBaseChange S f эквивалентно универсальному свойству подъема по отношению ко всем Q; существование и уникальность подъемов характеризуют базовое изменение.
LaTeX
$$$ IsBaseChange S f \iff \forall Q, ExistsUnique (g' : M \to Q) \text{ s.t. } (g'.restrictScalars R) \circ f = g $$$
Lean4
theorem iff_lift_unique :
IsBaseChange S f ↔
∀ (Q : Type max v₁ v₂ v₃) [AddCommMonoid Q],
∀ [Module R Q] [Module S Q],
∀ [IsScalarTower R S Q], ∀ g : M →ₗ[R] Q, ∃! g' : N →ₗ[S] Q, (g'.restrictScalars R).comp f = g :=
⟨fun h => by
intro Q _ _ _ _ g
exact ⟨h.lift g, h.lift_comp g, fun g' e => h.algHom_ext' _ _ (e.trans (h.lift_comp g).symm)⟩,
IsBaseChange.of_lift_unique f⟩
