arrowCongr_comp — Mathlib

English

ArrowCongr is a linear equivalence between spaces of linear maps induced by a pair of linear isomorphisms.

Русский

ArrowCongr задаёт линейное эквив между пространствами отображений, индуцируемое парой линейных изоморфизмов.

LaTeX

$$$\text{arrowCongr } e_1 e_2 : (M_1 \to_{\sigma_{11}'} M_1') \simeq (M_2 \to_{\sigma_{22}'} M_2').$$$

Lean4

theorem arrowCongr_comp (e₁ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') (e₃ : M₁'' ≃ₛₗ[σ₁''₂''] M₂'')
    (f : M₁ →ₛₗ[σ₁₁'] M₁') (g : M₁' →ₛₗ[σ₁'₁''] M₁'') :
    arrowCongr e₁ e₃ (g.comp f) = (arrowCongr e₂ e₃ g).comp (arrowCongr e₁ e₂ f) :=
  by
  ext
  simp only [symm_apply_apply, arrowCongr_apply, LinearMap.comp_apply]

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