of_comp — Mathlib

English

Given an equivalence e: M ≃ N that realizes the base change, IsBaseChange S f holds.

Русский

Дано эквивалентность e: M ≃ N, реализующая базовое изменение, и IsBaseChange S f выполняется.

LaTeX

$$$ IsBaseChange S f \leftarrow e: M \simeq N$$$

Lean4

/-- If `N` is the base change of `M` to `S` and `O` the base change of `M` to `T`, then
`O` is the base change of `N` to `T`. -/
theorem of_comp {f : M →ₗ[R] N} (hf : IsBaseChange S f) {h : N →ₗ[S] O} (hc : IsBaseChange T ((h : N →ₗ[R] O) ∘ₗ f)) :
    IsBaseChange T h := by
  apply IsBaseChange.of_lift_unique
  intro Q _ _ _ _ r
  letI : Module R Q := inferInstanceAs (Module R (RestrictScalars R S Q))
  haveI : IsScalarTower R S Q := IsScalarTower.of_algebraMap_smul fun r ↦ congrFun rfl
  haveI : IsScalarTower R T Q :=
    IsScalarTower.of_algebraMap_smul fun r x ↦ by simp [IsScalarTower.algebraMap_apply R S T]
  let r' : M →ₗ[R] Q := r ∘ₗ f
  let q : O →ₗ[T] Q := hc.lift r'
  refine ⟨q, ?_, ?_⟩
  · apply hf.algHom_ext'
    simp [r', q, LinearMap.comp_assoc, hc.lift_comp]
  · intro q' hq'
    apply hc.algHom_ext'
    apply_fun LinearMap.restrictScalars R at hq'
    rw [← LinearMap.comp_assoc]
    rw [show q'.restrictScalars R ∘ₗ h.restrictScalars R = _ from hq', hc.lift_comp]

Похожие утверждения