English
Precomposing with a finite-type equivalence preserves the triviality of the relation: IsTrivialRelation (f ∘ e) (x ∘ e) ↔ IsTrivialRelation f x.
Русский
Сжатие с использованием эквивалентности конечного типа сохраняет тривиальность: IsTrivialRelation (f ∘ e) (x ∘ e) ↔ IsTrivialRelation f x.
LaTeX
$$IsTrivialRelation (f ∘ e) (x ∘ e) ↔ IsTrivialRelation f x$$
Lean4
/-- The proposition that the relation $\sum_i f_i x_i = 0$ in $M$ is trivial.
That is, there exist a finite index type $\kappa$ = `Fin k`, elements
$(y_j)_{j \in \kappa}$ of $M$, and elements $(a_{ij})_{i \in \iota, j \in \kappa}$ of $R$
such that for all $i$,
$$x_i = \sum_j a_{ij} y_j$$
and for all $j$,
$$\sum_i f_i a_{ij} = 0.$$
By `Module.sum_smul_eq_zero_of_isTrivialRelation`, this condition implies $\sum_i f_i x_i = 0$. -/
abbrev IsTrivialRelation : Prop :=
∃ (k : ℕ) (a : ι → Fin k → R) (y : Fin k → M), (∀ i, x i = ∑ j, a i j • y j) ∧ ∀ j, ∑ i, f i * a i j = 0
