<commit_before>/-
Copyright (c) 2018 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: <NAME>
-/
import algebra.module
import ring_theory.maps

/-!
# Sesquilinear form

This file defines a bilinear form over a module. The definition requires a ring antiautomorphism
on the scalar ring, which comes from the file ring_theory.involution. Basic ideas such as
orthogonality are also introduced.

A sesquilinear form on an R-module M, is a function from M x M to R, that is linear in the first argument
and antilinear in the second, with respect to an antiautomorphism on R (an antiisomorphism from R to R).

## Notations

Given any term S of type sesq_form, due to a coercion, can use the notation S x y to
refer to the function field, ie. S x y = S.bilin x y.

## References

* <https://en.wikipedia.org/wiki/Sesquilinear_form#Over_arbitrary_rings>

## Tags

Sesquilinear form,
-/

open ring_anti_equiv

universes u v

/-- A sesquilinear form over a module  -/
structure sesq_form (R : Type u) (M : Type v) [ring R] (I : ring_anti_equiv R R) [add_comm_group M] [module R M] :=
(sesq : M → M → R)
(sesq_add_left : ∀ (x y z : M), sesq (x + y) z = sesq x z + sesq y z)
(sesq_smul_left : ∀ (a : R) (x y : M), sesq (a • x) y = a * (sesq x y))
(sesq_add_right : ∀ (x y z : M), sesq x (y + z) = sesq x y + sesq x z)
(sesq_smul_right : ∀ (a : R) (x y : M), sesq x (a • y) = (I a) * (sesq x y))

namespace sesq_form

section general_ring
variables {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : ring_anti_equiv R R} {S : sesq_form R M I}

instance : has_coe_to_fun (sesq_form R M I) :=<commit_msg>docs(linear_algebra/sesquilinear_form): correct module docs (#2757)<commit_after>/-
Copyright (c) 2018 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: <NAME>
-/
import algebra.module
import ring_theory.maps

/-!
# Sesquilinear form

This file defines a sesquilinear form over a module. The definition requires a ring antiautomorphism
on the scalar ring, which comes from the file ring_theory.involution. Basic ideas such as
orthogonality are also introduced.

A sesquilinear form on an R-module M, is a function from M x M to R, that is linear in the first argument
and antilinear in the second, with respect to an antiautomorphism on R (an antiisomorphism from R to R).

## Notations

Given any term S of type sesq_form, due to a coercion, can use the notation S x y to
refer to the function field, ie. `S x y = S.sesq x y`.

## References

* <https://en.wikipedia.org/wiki/Sesquilinear_form#Over_arbitrary_rings>

## Tags

Sesquilinear form,
-/

open ring_anti_equiv

universes u v

/-- A sesquilinear form over a module  -/
structure sesq_form (R : Type u) (M : Type v) [ring R] (I : ring_anti_equiv R R) [add_comm_group M] [module R M] :=
(sesq : M → M → R)
(sesq_add_left : ∀ (x y z : M), sesq (x + y) z = sesq x z + sesq y z)
(sesq_smul_left : ∀ (a : R) (x y : M), sesq (a • x) y = a * (sesq x y))
(sesq_add_right : ∀ (x y z : M), sesq x (y + z) = sesq x y + sesq x z)
(sesq_smul_right : ∀ (a : R) (x y : M), sesq x (a • y) = (I a) * (sesq x y))

namespace sesq_form

section general_ring
variables {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : ring_anti_equiv R R} {S : sesq_form R M I}

instance : has_coe_to_fun (sesq_form R M I) :=
{'fraction_non_alphanumeric': 0.10711124225435231, 'fraction_numerical': 0.00472115668338743, 'mean_word_length': 3.6311475409836067, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 9, 'https://': 2, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6876337', 'n_tokens_mistral': 1323, 'n_tokens_neox': 1245, 'n_words': 548}