Systems of quadratic forms

DefinitionOrthogonal sum of systems of quadratic forms#✓fully proved

Let \(R\) be a commutative semiring, let \(M\) and \(N\) be \(R\)-modules, and let \((Q_i)_{i \in \iota}\) and \((Q'_i)_{i \in \iota}\) be families of quadratic forms on \(M\) and on \(N\) indexed by the same type \(\iota\). Their pointwise orthogonal sum is the family \((Q_i \oplus Q'_i)_{i \in \iota}\) of quadratic forms on \(M \times N\), where \(Q_i \oplus Q'_i\) is the orthogonal sum given by \((Q_i \oplus Q'_i)(x, y) = Q_i(x) + Q'_i(y)\).

def systemOrthogonalSum (Q : ι → QuadraticForm R M) (Q' : ι → QuadraticForm R N) :
    ι → QuadraticForm R (M × N) :=
  fun i ↦ (Q i).prod (Q' i)

Used by 3

Used byEvaluating an orthogonal sum of systems of quadratic forms · Orthogonal sum of systems on the left summand · Orthogonal sum of systems on the right summand

TheoremEvaluating an orthogonal sum of systems of quadratic forms#✓fully proved

Let \(R\) be a commutative semiring, let \(M\) and \(N\) be \(R\)-modules, and let \((Q_i)_{i \in \iota}\) and \((Q'_i)_{i \in \iota}\) be families of quadratic forms on \(M\) and on \(N\) indexed by the same type \(\iota\). For every index \(i\) and every \((x, y) \in M \times N\), the \(i\)-th form of their pointwise orthogonal sum takes the value \(Q_i(x) + Q'_i(y)\) at \((x, y)\).

@[simp]
theorem systemOrthogonalSum_apply (Q : ι → QuadraticForm R M)
    (Q' : ι → QuadraticForm R N) (i : ι) (x : M × N) :
    systemOrthogonalSum Q Q' i x = Q i x.1 + Q' i x.2

Uses 1 · Used by 2

Statement usesOrthogonal sum of systems of quadratic forms

Used byOrthogonal sum of systems on the left summand · Orthogonal sum of systems on the right summand

TheoremOrthogonal sum of systems on the left summand#✓fully proved

Let \(R\) be a commutative semiring, let \(M\) and \(N\) be \(R\)-modules, and let \((Q_i)_{i \in \iota}\) and \((Q'_i)_{i \in \iota}\) be families of quadratic forms on \(M\) and on \(N\) indexed by the same type \(\iota\). For every index \(i\) and every \(x \in M\), the \(i\)-th form of their pointwise orthogonal sum takes the value \(Q_i(x)\) at \((x, 0) \in M \times N\).

@[simp]
theorem systemOrthogonalSum_inl (Q : ι → QuadraticForm R M)
    (Q' : ι → QuadraticForm R N) (i : ι) (x : M) :
    systemOrthogonalSum Q Q' i (x, 0) = Q i x

Uses 2

Statement usesOrthogonal sum of systems of quadratic forms

Proof usesEvaluating an orthogonal sum of systems of quadratic forms

TheoremOrthogonal sum of systems on the right summand#✓fully proved

Let \(R\) be a commutative semiring, let \(M\) and \(N\) be \(R\)-modules, and let \((Q_i)_{i \in \iota}\) and \((Q'_i)_{i \in \iota}\) be families of quadratic forms on \(M\) and on \(N\) indexed by the same type \(\iota\). For every index \(i\) and every \(y \in N\), the \(i\)-th form of their pointwise orthogonal sum takes the value \(Q'_i(y)\) at \((0, y) \in M \times N\).

@[simp]
theorem systemOrthogonalSum_inr (Q : ι → QuadraticForm R M)
    (Q' : ι → QuadraticForm R N) (i : ι) (y : N) :
    systemOrthogonalSum Q Q' i (0, y) = Q' i y

Uses 2

Statement usesOrthogonal sum of systems of quadratic forms

Proof usesEvaluating an orthogonal sum of systems of quadratic forms

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.