Theorems · Definition · commutative algebra

Module.IsTrivialRelation

{R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [Module R M] → {ι : Type u_3} → [Fintype ι] → (ι → R) → (ι → M) → Prop

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$.

Defined in

Mathlib.RingTheory.Flat.EquationalCriterion

Cited by

9 results in Mathlib

Foundations

Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleFintype