Skip to content

[Merged by Bors] - doc(LinearAlgebra): fix typos #37341

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
harahu wants to merge 1 commit into from
+13 −13
Closed

[Merged by Bors] - doc(LinearAlgebra): fix typos #37341

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 11 additions & 11 deletions Mathlib/LinearAlgebra/Center.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,13 +21,13 @@ the center of `Module.End R V`.
In what follows, `V` is assumed to be a free `R`-module.
* `LinearMap.commute_transvections_iff_of_basis`:
if an endomorphism `f : V →ₗ[R] V` commutes with every elementary transvections
(in a given basis), then it is an homothety with central ratio.
if an endomorphism `f : V →ₗ[R] V` commutes with every elementary transvection
(in a given basis), then it is a homothety with central ratio.
(Assumes that the basis is provided and has a non trivial set of indices.)
* `LinearMap.exists_eq_smul_id_of_forall_notLinearIndependent`:
over a commutative ring `R` which is a domain, an endomorphism `f : V →ₗ[R] V`
of a free domain such that `v` and `f v` are not linearly independent,
of a free module such that `v` and `f v` are not linearly independent,
for all `v : V`, is a homothety.
* `LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent`:
Expand All @@ -41,7 +41,7 @@ In what follows, `V` is assumed to be a free `R`-module.
Note. In the noncommutative case, the last two results do not hold
when the rank is equal to 1. Indeed, right multiplications
with noncentral ratio of the `R`-module `R` satisfy the property
that `f v` and `v` are linearly independent, for all `v : V`,
that `f v` and `v` are linearly dependent, for all `v : V`,
but they are not left multiplication by some element.
-/
Expand Down Expand Up @@ -92,17 +92,17 @@ theorem commute_transvections_iff_of_basis

set_option backward.isDefEq.respectTransparency false in
/-- Over a domain, an endomorphism `f` of a free module `V`
of rank ≠ 1 such that `f v` and `v` are colinear, for all `v : V`,
of rank ≠ 1 such that `f v` and `v` are collinear, for all `v : V`,
consists of homotheties with central ratio.
In the commutative case, use `LinearMap.exists_eq_smul_id`.
This is a variant of `LinearMap.exists_mem_center_apply_smul`
which switches the use `StrongRankInduction` and `finrank`
which switches the use of `StrongRankInduction` and `finrank`
for the cardinality of a given basis.
When `finrank R V = 1`, up to a linear equivalence `V ≃ₗ[R] R`,
then any `f` is *right*-multiplication by some `a : K`,
then any `f` is *right*-multiplication by some `a : R`,
but not necessarily *left*-multiplication by an element of the center of `R`. -/
theorem exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis
[Ring R] [IsDomain R] [AddCommGroup V] [Module R V]
Expand Down Expand Up @@ -181,14 +181,14 @@ theorem exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis

set_option backward.isDefEq.respectTransparency false in
/-- Over a domain `R`, an endomorphism `f` of a free module `V`
of rank ≠ 1 such that `f v` and `v` are colinear, for all `v : V`,
of rank ≠ 1 such that `f v` and `v` are collinear, for all `v : V`,
consists of homotheties with central ratio.
When `R`does not satisfy `StrongRankCondition`, use
When `R` does not satisfy `StrongRankCondition`, use
`LinearMap.exists_mem_center_apply_eq_smul_of_basis`.
When `finrank R V = 1`, up to a linear equivalence `V ≃ₗ[R] R`,
then any `f` is *right*-multiplication by some `a : K`,
then any `f` is *right*-multiplication by some `a : R`,
but not necessarily *left*-multiplication by an element of the center of `R`. -/
theorem exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent
[Ring R] [IsDomain R] [StrongRankCondition R]
Expand All @@ -210,7 +210,7 @@ theorem exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent
exact exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis b h

/-- Over a commutative domain, an endomorphism `f` of a free module `V`
such that `f v` and `v` are colinear, for all `v : V`,
such that `f v` and `v` are collinear, for all `v : V`,
consists of homotheties. -/
theorem exists_eq_smul_id_of_forall_notLinearIndependent
[CommRing R] [IsDomain R] [AddCommGroup V] [Module R V] [Free R V] {f : V →ₗ[R] V}
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/LinearAlgebra/JordanChevalley.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,10 +17,10 @@ sufficient condition for there to exist a nilpotent endomorphism `n` and a semis
`s`, such that `f = n + s` and both `n` and `s` are polynomial expressions in `f`.

The condition is that there exists a separable polynomial `P` such that the endomorphism `P(f)` is
nilpotent. This condition is always satisfied when the coefficients are a perfect field.
nilpotent. This condition is always satisfied when the coefficient field is perfect.

The proof given here uses Newton's method and is taken from Chambert-Loir's notes:
[Algebre](http://webusers.imj-prg.fr/~antoine.chambert-loir/enseignement/2022-23/agreg/algebre.pdf)
[Algèbre](http://webusers.imj-prg.fr/~antoine.chambert-loir/enseignement/2022-23/agreg/algebre.pdf)

## Main definitions / results:

Expand Down
Loading