QuadraticForm.Isometry.ext
theorem QuadraticForm.Isometry.ext :
∀ {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
[inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {Q₁ : QuadraticForm R M₁}
{Q₂ : QuadraticForm R M₂} ⦃f g : Q₁.Isometry Q₂⦄, (∀ (x : M₁), f x = g x) → f = g
This theorem, labeled `QuadraticForm.Isometry.ext`, asserts that for any types `R`, `M₁`, and `M₂` with `R` being a commutative semiring and `M₁`, `M₂` being modules over `R`, and for any quadratic forms `Q₁` on `M₁` and `Q₂` on `M₂`, if two isometric maps `f` and `g` from `Q₁` to `Q₂` coincide on every point in `M₁`, then `f` and `g` are indeed the same map. In other words, the uniqueness of an isometry between two quadratic forms is determined by its action on all elements of the domain.
More concisely: If two isometric maps between quadratic forms over a commutative semiring and their modules coincide on all domain elements, then they are equal.
|
QuadraticForm.Isometry.map_app'
theorem QuadraticForm.Isometry.map_app' :
∀ {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
[inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {Q₁ : QuadraticForm R M₁}
{Q₂ : QuadraticForm R M₂} (self : Q₁.Isometry Q₂) (m : M₁), Q₂ (self.toFun m) = Q₁ m
This theorem states that for any commutative semiring `R`, additive commutative monoids `M₁` and `M₂`, and given that `M₁` and `M₂` are both `R`-modules. If there exists an isometry `self` between two quadratic forms `Q₁` and `Q₂` over `M₁` and `M₂` respectively, then the value of `Q₂` at the image of any element `m` under the isometry is the same as the value of `Q₁` at `m`. In other words, this isometry preserves the quadratic form.
More concisely: For any commutative semiring `R`, isometries between quadratic forms `Q₁` and `Q₂` over `R`-modules `M₁` and `M₂`, respectively, preserve the values of the quadratic forms, i.e., `Q₁(m) = Q₂(self(m))` for all `m` in `M₁`.
|