English
If a lifting property holds for all Q in a base-change context, then IsBaseChange S f holds; uniqueness of lift ensures the base-change characterization.
Русский
Если существует тензорное поднятие для всех Q в контексте базового изменения и единственность поднятия, то IsBaseChange S f выполняется; уникальность обеспечивает характеристику базового изменения.
LaTeX
$$$ IsBaseChange \; (f) \; \Rightarrow \exists! \text{lift} \, g \; (Restricted) $$$
Lean4
theorem of_lift_unique
(h :
∀ (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) :
IsBaseChange S f :=
by
obtain ⟨g, hg, -⟩ := h (ULift.{v₂} <| S ⊗[R] M) (ULift.moduleEquiv.symm.toLinearMap.comp <| TensorProduct.mk R S M 1)
let f' : S ⊗[R] M →ₗ[R] N :=
TensorProduct.lift
(((LinearMap.flip (AlgHom.toLinearMap (Algebra.ofId S (Module.End S (M →ₗ[R] N))))) f).restrictScalars R)
change Function.Bijective f'
let f'' : S ⊗[R] M →ₗ[S] N :=
by
refine
{ f' with
map_smul' := fun s x => TensorProduct.induction_on x ?_ (fun s' y => smul_assoc s s' _) fun x y hx hy => ?_ }
· dsimp; rw [map_zero, smul_zero, map_zero, smul_zero]
· dsimp at *; rw [smul_add, map_add, map_add, smul_add, hx, hy]
simp_rw [DFunLike.ext_iff, LinearMap.comp_apply, LinearMap.restrictScalars_apply] at hg
let fe : S ⊗[R] M ≃ₗ[S] N := LinearEquiv.ofLinear f'' (ULift.moduleEquiv.toLinearMap.comp g) ?_ ?_
· exact fe.bijective
· rw [← LinearMap.cancel_left (ULift.moduleEquiv : ULift.{max v₁ v₃} N ≃ₗ[S] N).symm.injective]
refine (h (ULift.{max v₁ v₃} N) <| ULift.moduleEquiv.symm.toLinearMap.comp f).unique ?_ rfl
ext x
simp only [LinearMap.comp_apply, LinearMap.restrictScalars_apply, hg]
apply one_smul
· ext x
change (g <| (1 : S) • f x).down = _
rw [one_smul, hg]
rfl
