algHom_ext — Mathlib

English

If f is a base change and h is a base change for N → O, then the composed map h ∘ f is a base change for N → O, under a compatible tower of scalars.

Русский

Если f — базовое изменение и h — базовое изменение для N → O, то композиция h ∘ f является базовым изменением для N → O при совместимой цепи скаляров.

LaTeX

$$$ IsBaseChange S f \to IsBaseChange T ((h : N \to O) \circ f) $$$

Lean4

theorem algHom_ext (g₁ g₂ : N →ₗ[S] Q) (e : ∀ x, g₁ (f x) = g₂ (f x)) : g₁ = g₂ :=
  by
  ext x
  refine h.inductionOn x _ ?_ ?_ ?_ ?_
  · rw [map_zero, map_zero]
  · assumption
  · intro s n e'
    rw [g₁.map_smul, g₂.map_smul, e']
  · intro x y e₁ e₂
    rw [map_add, map_add, e₁, e₂]

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