QuadraticForm.anisotropic_of_pi
theorem QuadraticForm.anisotropic_of_pi :
∀ {ι : Type u_1} {Mᵢ : ι → Type u_7} [inst : (i : ι) → AddCommMonoid (Mᵢ i)] [inst_1 : Fintype ι] {R : Type u_9}
[inst_2 : OrderedCommRing R] [inst_3 : (i : ι) → Module R (Mᵢ i)] {Q : (i : ι) → QuadraticForm R (Mᵢ i)},
(QuadraticForm.pi Q).Anisotropic → ∀ (i : ι), (Q i).Anisotropic
This theorem states that if a quadratic form defined on a family of modules is anisotropic, then each of the quadratic forms defined on the individual modules is also anisotropic. Here, "anisotropic" means that the quadratic form evaluates to zero if and only if the input is zero. However, the converse is not true; it doesn't follow that if every individual component is anisotropic, then the whole family is anisotropic. This is defined over any ordered commutative ring `R` and for any indexing set `ι`.
More concisely: If a quadratic form on a family of modules over an ordered commutative ring evaluates to zero only for the zero input, then each quadratic form on an individual module also evaluates to zero only for the zero input (anisotropy is not preserved under taking direct sums).
|
QuadraticForm.anisotropic_of_prod
theorem QuadraticForm.anisotropic_of_prod :
∀ {M₁ : Type u_3} {M₂ : Type u_4} [inst : AddCommMonoid M₁] [inst_1 : AddCommMonoid M₂] {R : Type u_9}
[inst_2 : OrderedCommRing R] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {Q₁ : QuadraticForm R M₁}
{Q₂ : QuadraticForm R M₂}, (Q₁.prod Q₂).Anisotropic → Q₁.Anisotropic ∧ Q₂.Anisotropic
The theorem states that if a product of two quadratic forms is anisotropic, then each of the quadratic forms that make up the product must also be anisotropic. The term 'anisotropic' here refers to the property of a quadratic form that it does not take the value zero other than at the zero vector. The theorem is applicable over an ordered commutative ring and assumes that the quadratic forms act on modules over this ring. Note that the converse of this statement, that if the components are anisotropic then their product is as well, is not necessarily true.
More concisely: If two quadratic forms over an ordered commutative ring, whose modules they act on, have an anisotropic product, then each of the forms is anisotropic.
|
QuadraticForm.pi_apply
theorem QuadraticForm.pi_apply :
∀ {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_7} [inst : CommSemiring R]
[inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)] [inst_2 : (i : ι) → Module R (Mᵢ i)] [inst_3 : Fintype ι]
(Q : (i : ι) → QuadraticForm R (Mᵢ i)) (x : (i : ι) → Mᵢ i),
(QuadraticForm.pi Q) x = Finset.univ.sum fun i => (Q i) (x i)
This theorem states that for a family of quadratic forms `Q : (i : ι) → QuadraticForm R (Mᵢ i)` on a family of modules `Mᵢ : ι → Type u_7` over a commutative semiring `R`, and for any vector `x : (i : ι) → Mᵢ i` (which is indexed by the same type `ι`), the value of the quadratic form constructed via `QuadraticForm.pi` at `x` is equal to the sum, taken over all indices in `ι`, of each `Q i` evaluated at `x i`. In other words, the quadratic form on the entire family of modules evaluates to the sum of the evaluations of the individual quadratic forms.
More concisely: For a family of quadratic forms `Q : (i : ι) → QuadraticForm R (Mᵢ i)` on modules `Mᵢ : ι → Type u_7` over a commutative semiring `R`, the quadratic form `∏ i, Q i` evaluated at the vector `x : (i : ι) → Mᵢ i` equals the sum `∑ i, Q i x i`.
|