English
The constr operator acts as the identity when the function sends i to f(b i).
Русский
Оператор constr действует как тождественный при соответствующем отображении.
LaTeX
$$$(\\mathrm{constr}\\, b\\ S\\ (i \\mapsto f(b i))) = f.$$$
Lean4
/-- If `b` is a basis for `M` and `b'` a basis for `M'`,
and `f`, `g` form a bijection between the basis vectors,
`b.equiv' b' f g hf hg hgf hfg` is a linear equivalence `M ≃ₗ[R] M'`, mapping `b i` to `f (b i)`.
-/
def equiv' (f : M → M') (g : M' → M) (hf : ∀ i, f (b i) ∈ range b') (hg : ∀ i, g (b' i) ∈ range b)
(hgf : ∀ i, g (f (b i)) = b i) (hfg : ∀ i, f (g (b' i)) = b' i) : M ≃ₗ[R] M' :=
{ constr (M' := M') b R (f ∘ b) with
invFun := constr (M' := M) b' R (g ∘ b')
left_inv :=
have : (constr (M' := M) b' R (g ∘ b')).comp (constr (M' := M') b R (f ∘ b)) = LinearMap.id :=
b.ext fun i =>
Exists.elim (hf i) fun i' hi' => by
rw [LinearMap.comp_apply, b.constr_basis, Function.comp_apply, ← hi', b'.constr_basis, Function.comp_apply,
hi', hgf, LinearMap.id_apply]
fun x => congr_arg (fun h : M →ₗ[R] M => h x) this
right_inv :=
have : (constr (M' := M') b R (f ∘ b)).comp (constr (M' := M) b' R (g ∘ b')) = LinearMap.id :=
b'.ext fun i =>
Exists.elim (hg i) fun i' hi' => by
rw [LinearMap.comp_apply, b'.constr_basis, Function.comp_apply, ← hi', b.constr_basis, Function.comp_apply,
hi', hfg, LinearMap.id_apply]
fun x => congr_arg (fun h : M' →ₗ[R] M' => h x) this }
