Access the full text.
Sign up today, get DeepDyve free for 14 days.
Pavel Etingof (2008)
LIE GROUPS AND LIE ALGEBRASLie Groups, Lie Algebras, and Cohomology. (MN-34), Volume 34
Jean-Pierre Serre (1987)
Complex Semisimple Lie Algebras
Oliver Nash (2021)
Formalising lie algebrasProceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs
N Jacobson (1952)
Une généralisation du théorème d’EngelC. R. Acad. Sci. Paris, 234
F. Dupuis, R. Lewis, H. Macbeth (2022)
Formalized functional analysis with semilinear maps
M. Jacobson, M. Hadamard (1989)
algèbre. — Une généralisation du théorème d’Engel.
(2019)
The type theory of lean, 2019
M. Zorn (1937)
On a theorem of EngelBulletin of the American Mathematical Society, 43
The Community (2019)
The lean mathematical libraryProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs
W. Fisher (1920)
Translated from the FrenchSchool Science and Mathematics, 20
E. Zelmanov (1991)
SOLUTION OF THE RESTRICTED BURNSIDE PROBLEM FOR GROUPS OF ODD EXPONENTMathematics of The Ussr-izvestiya, 36
Gabriele Torre (2010)
Representation theory
koltsakh Li, Dan Sssr (2018)
E. I. Zel’manov Solution of the restricted Burnside problem for groups of odd exponent
Publisher's Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations
any non-empty subset of Lie subalgebras contains a maximal element
We discuss the theory of Lie algebras in Lean’s Mathlib library. Using nilpotency as the theme, we outline a computer formalisation of Engel’s theorem and an application to root space theory. We emphasise that all arguments work with coefﬁcients in any commutative ring. Keywords Lean · Proof assistant · Formal math · Lie algebra · Nilpotency · Engel’s theorem · Root space Mathematics Subject Classiﬁcation 17B30 · 68V15 · 68V20 1 Introduction In previous work [6], we reported on the formalisation of Lie algebras in Lean’s Mathlib library [8]. Whereas the aim of [6] was to give a high-level overview of the state of Mathlib’s Lie theory, our goal here is to use a particular aspect of Lie theory (nilpotency) as a means for illustrating two of Mathlib’s most important virtues: generality and unity. For example we shall see that Mathlib’s version of Engel’s theorem uniﬁes the various versions of this result appearing in the informal literature, while demanding weaker hypotheses and providing a stronger result. This article also presents an opportunity to highlight certain additions to Mathlib’s Lie algebra theory that have been made since [6]. To be precise, Mathlib’s Lie theory has grown from c.6000 lines to c.7500 lines since [6]. The most important additions are the proof of Engel’s theorem and its corollary (4) characterising Cartan subalgebras. We brieﬂy summarise some key context and refer the reader to the references for further discussion. Lean is an open-source, dependently-typed functional programming language and proof assistant. The principal developer is Leonardo de Moura at Microsoft Research. It uses a type theory similar to that of Coq for its logical foundation, see e.g., [2]. Mathlib [8] is an open-source, massively-collaborative library of formal mathematics writ- ten using Lean. As of June 2022, it contains c.900,000 lines of code, is steadily growing, and contains large quantities of contemporary undergraduate- and graduate-level mathematics. B Oliver Nash o.nash@imperial.ac.uk Department of Mathematics, Imperial College, London, UK 0123456789().: V,-vol 123 18 Page 2 of 10 O. Nash Lie algebras are an important class of algebras which arise throughout mathematics and physics. Well-known to geometers as an abstraction of inﬁnitesimal symmetry, Lie algebras show up throughout mathematics, occupying prominent roles across the subject, from number theory to differential geometry. They are also essential for understanding much of 20th Century physics, especially the Standard Model in particle physics. In addition, the beautiful classiﬁcation of semisimple Lie algebras and their representations has made them an object of study in their own right. As outlined in [6], Mathlib contains a substantial body of Lie algebra theory. The starting point is a pair of typeclasses which permit one to make the statement that a type L carries the structure of a Lie algebra over a commutative ring R. For the beneﬁt of non-specialists we emphasise that Lie rings are not required to be associative and so are not rings in the sense in which the term is most often used. The formal deﬁnitions in Mathlib are as follows [src]: class lie_ring (L : Type v) extends add_comm_group L, has_bracket L L := (add_lie : ∀ (x y z : L), x + y,z = x,z + y,z ) (lie_add : ∀ (x y z : L), x,y + z = x,y + x,z ) (lie_self : ∀ (x : L), x,x = 0) (leibniz_lie : ∀ (x y z : L), x, y,z = x,y ,z + y, x,z ) class lie_algebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] extends module R L := (lie_smul : ∀ (t : R) (x y : L), x,t · y = t · x,y ) We emphasise that no assumptions are made about the coefﬁcients R except that they form a commutative ring. Practictioners of formal mathematics will be familiar with the value of making deﬁnitions as general as reasonably possible. Of course, if one also seeks to make theorems correspondingly general, then new arguments are often required. One of the points of this article is that this extra effort may yield unexpected beneﬁts. Our case study is Engel’s theorem which turns out to be true for any commutative ring R and to apply to a generalisation of nilpotency to Lie modules. As we shall see, the generalisation of nilpotency, from algebras to modules, is especially convenient as it uniﬁes the various versions of Engel’s theorem that appear in the literature. In addition we obtain a slightly more powerful result; this is useful when it comes to applications and we give an example of this for root spaces in Sect. 5. 2 Lie Modules Given a Lie algebra L, Mathlib’s deﬁnition of a Lie module M of L is [src]: class lie_ring_module (L : Type v) (M : Type w) [lie_ring L] [add_comm_group M] extends has_bracket L M := (add_lie : ∀ (x y : L) (m : M), x+y,m = x,m + y,m ) (lie_add : ∀ (x : L) (m n : M), x,m+n = x,m + x,n ) (leibniz_lie : ∀ (x y : L) (m : M), x, y, m = x, y ,m + y, x, m ) I.e., with coefﬁcients in. Associative Lie rings with a non-trivial product are rare and rather uninteresting. A Lie module M is also known as a representation of a Lie algebra L and it is synonymous to say that M is a module ‘of’ L or a module ‘over’ L. 123 Engel’s Theorem in Mathlib Page 3 of 10 18 class lie_module (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] := (smul_lie : ∀ (t : R) (x : L) (m : M), t · x, m = t · x, m ) (lie_smul : ∀ (t : R) (x : L) (m : M), x, t · m = t · x, m ) Observe that we denote the action of an element x of a Lie algebra L on an element m of a Lie module M by [x , m]. This permits a uniform notation when regarding a Lie algebra as a module over itself. The action of L on M induces a natural map: φ : L → End(M ) x → φ , deﬁned by: φ =[x , m]. In Mathlib this is [src]: def lie_module.to_endomorphism : L → R module.End R M := { to_fun := λ x, { to_fun := λ m, x, m , -- etc. }} Any Lie algebra acts on itself and in this special case, when M = L,the map φ is known as the adjoint action, and is denoted [src]: ad : L → End(L) x → ad . 3 Nilpotency Nilpotency is an important concept in algebra, with applications beyond what one might naïvely expect from the deﬁnitions. In the case of Lie algebras, the representation theory of nilpotent Lie algebras is both especially simple and especially important since semisimple Lie algebras are best understood as representations of certain nilpotent subalgebras, namely, Cartan subalgebras. 3.1 Ideal Operations and Nilpotent Lie Modules Given a Lie module M of a Lie algebra L, recall ([6] section 3) that for any ideal I ⊆ L and Lie submodule N ⊆ M we can form a new Lie submodule [src]: [I , N]⊆ M . It is the smallest Lie submodule of M containing all elements of the form [x , m] for all x ∈ I and m ∈ N . I.e., is a module over itself. Most of the theory of semisimple Lie algebras has yet to be formalised. Adding this material to Mathlib following, say [7], would be a worthy endeavour. 123 18 Page 4 of 10 O. Nash Informally, the lower central series of a Lie module M is the sequence of Lie submodules of M deﬁned recursively as: C M = M , C M =[L, C M ]. k+1 k The corresponding deﬁnitions in Mathlib are [src]: def lcs (k : N) : lie_submodule R L M → lie_submodule R L M := (λ N, ( : lie_ideal R L), N )^[k] def lower_central_series (k : N) : lie_submodule R L M := ( : lie_submodule R L M).lcs k Seealsothe ﬁnal paragraphofsection3in[6]. The lower central series is important because it provides a convenient way to deﬁne nilpotency [src]: class is_nilpotent : Prop := (nilpotent : ∃ k, lower_central_series RLMk = ⊥) Unwinding the deﬁnitions, informally a Lie module M is nilpotent if and only if there exists a natural number k such that for any x , x ,..., x in L and any m in M: 1 2 k [x , [x ,..., [x , m]···]] = 0. (1) 1 2 k We shall need the following property of a nilpotent Lie module: if M is non-trivial then it contains a non-zero element m such that: [x , m ]=0forall x in L.(2) Indeed one chooses a minimal k satisfying (1) and takes any non-zero element of the form: m =[x , [x ,..., [x , m]···]]. 0 2 3 k The result appears in Mathlib as [src]: lemma nontrivial_max_triv_of_is_nilpotent [nontrivial M] [is_nilpotent R L M] : nontrivial $ max_triv_submodule R L M := together with [src]: lemma mem_max_triv_submodule (m : M) : m ∈ max_triv_submodule R L M ↔∀ (x : L), x, m = 0 := 0 0 3.2 Acting Nilpotently An element a of an associative ring A is said to be nilpotent if there exists a natural number k such that: a = 0. Given a Lie module M of a Lie algebra L, this concept of nilpotency for elements of the ring A = End(M ) plays a central role in Engel’s theorem: We note in passing that the concept generalises to non-associative rings and that the relation [x , x]= 0 means that all elements x of a Lie algebra are nilpotent (taking k = 2). This fact is partly responsible for the elevated role that nilpotency plays in Lie theory. 123 Engel’s Theorem in Mathlib Page 5 of 10 18 Deﬁnition We say a Lie algebra L acts nilpotently on a Lie module M if the image of the natural map: φ : L → End(M ) x → φ , contains only nilpotent elements. A trivial but important observation is that if M is a nilpotent Lie module then L acts nilpotently. Indeed, given any x in L, taking the constant sequence: x = x = ··· = x = x , 1 2 k Equation (1) reads φ (m) = 0for any m, and thus: φ = 0. In Mathlib this statement is written [src]: lemma nilpotent_endo_of_nilpotent_module [is_nilpotent R L M] : ∃ (k : N), ∀ (x : L), (to_endomorphism RLMx)^k = 0 := A corollary of Engel’s theorem states that when L is Noetherian as an R-module, the converse statement holds. More precisely: k k ∀x , ∃k,φ = 0 ⇐⇒ ∃k, ∀x,φ = 0. x x 4 Engel’s Theorem Our goal is to outline a proof of: Theorem (Engel’s theorem) Let M be a Lie module over a Lie algebra L with coefﬁcients in a commutative ring R. Suppose that L is Noetherian as an R-module. Then M is nilpotent if and only if L acts nilpotently on M. The statement in Mathlib is [src]: lemma is_nilpotent_iff_forall [is_noetherian R L] : lie_module.is_nilpotent R L M ↔ ∀ x, is_nilpotent $ to_endomorphism R L M x := This should be compared with traditional versions appearing e.g. in Serre [7] (I.4, The- orems 1, 2, 2’), Bourbaki [1] (I, 4.2, Theorem 1, Corollaries 1, 3), Fulton, Harris, [4] (9.2, Theorem 9.9, Exercise 9.10). For the sake of deﬁniteness we give such a statement. Theorem (Engel’s theorem, traditional version) (a) Let L be a ﬁnite-dimensional Lie algebra with coefﬁcients in a ﬁeld. Then L is nilpotent if and only if it acts nilpotently on itself. (b) Let M be a non-trivial ﬁnite-dimensional vector space and suppose that L ⊆ End(M ) is a Lie subalgebra consisting of nilpotent elements. Then there exists a non-zero element m in M such that: [x , m ]= 0 for all x in L. Engel’s theorem is stronger because it applies for any x , x ,..., x , not just the constant sequence: x = 1 2 k 1 x = ··· = x = x. 2 k 123 18 Page 6 of 10 O. Nash Taking M = L in our version recovers part (a) in the traditional statement. As explained in the discussion of Eq. (2), part (b) is also a trivial corollary of our version. We have thus uniﬁed parts (a) and (b) in the traditional version into a single result. Demanding the stronger property that M is nilpotent also turns out to simplify the proof as we get a stronger inductive hypothesis at the key step in the proof. 4.1 Engelian Lie Algebras It is convenient to introduce some terminology. Deﬁnition We say a Lie algebra L is Engelian if any Lie module M on which L acts nilpo- tently is nilpotent. The deﬁnition in Mathlib is [src]: def lie_algebra.is_engelian : Prop := ∀ (M : Type u ) [add_comm_group M], by exactI ∀ [module R M] [lie_ring_module L M], by exactI ∀ [lie_module R L M], by exactI ∀ (h : ∀ x, is_nilpotent $ to_endomorphism R L M x), lie_module.is_nilpotent R L M In fact, this exposes a rough edge of Lean 3: quantiﬁcation over typeclasses requires use of the ‘by exactI ∀ pattern’ as well as the explicit mention of typeclasses that could be inferred (like add_comm_group, module etc). One would prefer to write simply ∀ (M: u ), [[lie_module R L M]] rather than the three lines appearing above. This situation is likely to improve after Mathlib is migrated to Lean 4. Using this new language, the non-trivial part of Engel’s theorem is the statement that Noetherian Lie algebras are Engelian: [src] lemma is_engelian_of_is_noetherian [is_noetherian R L] : lie_algebra.is_engelian R L := 4.2 Passing to the Image in End(M) We now ﬁx a Noetherian Lie algebra L together with a Lie module M on which it acts nilpotently. The ﬁrst step in the proof is to note that we may replace L with its image: L = range φ ⊆ End(M ), under the natural map: φ : L → End(M ). The relevant formal statement is [src]: lemma is_nilpotent_range_to_endomorphism_iff : is_nilpotent R (to_endomorphism R L M).range M ↔ is_nilpotent R L M := The universe u appearing is not signiﬁcant and merely reﬂects Mathlib’s standard universe polymorphism. Lean can handle such polymorphism automatically so one could (and probably should) replace Type u with Type*. 123 Engel’s Theorem in Mathlib Page 7 of 10 18 The proof is essentially tautological but the observation is important and the lemma is a good example of Lean’s typeclass mechanism working well. Without the user doing anything, Lean recognises that (to_endomorphism R L M).range, i.e. L , is a Lie algebra and that M is naturally a Lie module over L . All of this is achieved by typeclass instances registered far away, with no direct connection to Engel’s theorem. The passage from L to L is useful because of the following lemma [src]: lemma lie_algebra.is_nilpotent_ad_of_is_nilpotent {A : Type v} [comm_ring R] [ring A] [algebra R A] {L : lie_subalgebra R A} {x : L } (h : is_nilpotent (x : A)) : is_nilpotent $ lie_algebra.ad R L x := (Note that an associative algebra A is naturally also a Lie algebra [src] which is why we may write lie_subalgebra R A. See also [6] section 5.) The proof follows from the binomial theorem. Taking A = End(M ) the lemma states that L acts nilpotently on itself. 4.3 The Main Argument We introduce the set: s ={K ⊆ L | K is an Engelian Lie subalgebra}, written in Mathlib as [src]: let s := {K : lie_subalgebra R L | is_engelian R K }, Our goal is to show that s contains L , regarded as a Lie subalgebra of itself. This is the top element in the complete lattice of Lie subalgebras. Since s is non-empty (it contains the trivial Lie subalgebra) and L is Noetherian, s contains a maximal element. We thus need only show that an element of s cannot be maximal when it is a proper subalgebra. In other words we must justify the following claim appearing in the Mathlib proof [src]: have : ∀ (K ∈ s), K = →∃ (K ∈ s), K < K , Thus let K be a proper Engelian Lie subalgebra and consider the Lie module L /K over K . Because L acts nilpotently on itself, K ⊆ L acts nilpotently on L and thus also on L /K.Since K is Engelian, L /K is nilpotent and thus by (2) there exists x ∈ L − K such that: [K , x]⊆ K . (3) Finally let: K ={λx + μk | k ∈ K ; λ, μ ∈ R}. Using (3) and recalling that [x , x]= 0 we see that: • K is a Lie subalgebra of L , • K strictly contains K , • K is an ideal in K . To ﬁnish the argument we need only show that K is Engelian. We thus ﬁx a Lie module M over K on which K acts nilpotently. We must show that M is nilpotent. To do so, we apply the following lemma (whose proof is a simple induction) [src]: 123 18 Page 8 of 10 O. Nash lemma lcs_le_lcs_of_is_nilpotent_span_sup_eq_top {I : lie_ideal R L} {x : L} (hxI : (R • x) I = ) {nij : N} (hxn : (to_endomorphism R L M x)^n = 0) (hIM : lower_central_series R L M i ≤ I.lcs M j) : lower_central_series R L M (i + n) ≤ I.lcs M (j + 1) := with the roles of I , L played by K , K . We see that if the lower central series of M as a Lie module over K reaches zero, then its lower central central series over K must also reach zero. Thus nilpotency over K (which follows since K is Engelian) ensures nilpotency over K , as required. 5 The Zero Root Space As noted in [6] section 11, Mathlib contains deﬁnitions of and basic results about weight spaces and root spaces. Engel’s theorem was added to Mathlib for the purpose of advancing this theory. It may be instructive to outline this application. Given a nilpotent Lie subgalgebra H ⊆ L, a distinguished role is played by the zero root space. In Mathlib this is root_space H (0: H → R) [src]; informally it is: 0 k L ={x |∃k, ∀y ∈ H , ad (x ) = 0}⊆ L. Any root space is a H-submodule of L but more is true for the zero root space; it is a Lie subalgebra [src]: def zero_root_subalgebra : lie_subalgebra R L := { lie_mem := ..., .. (root_space H 0 : submodule R L) } 0 0 One always has H ⊆ L and it is easy to see that if H = L then H is a Cartan subalgebra. When L is Noetherian, Engel’s theorem shows that the converse holds: H = L ⇐⇒ H is a Cartan subalgebra. (4) The literature appears only to contain proofs of this result when the coefﬁcients are a ﬁeld. Moreover the arguments in the literature cannot be used since they argue inductively using dimension — a concept that does not exist over general coefﬁcients. Fortunately with our version of Engel’s theorem, the proof is almost trivial. Here is the statement of (4) in Mathlib [src]: lemma zero_root_subalgebra_eq_iff_is_cartan [is_noetherian R L]: zero_root_subalgebra R L H = H ↔ H.is_cartan_subalgebra := The point is that if L is Noetherian, then H acts nilpotently on L andsobyEngel’s theorem, L is nilpotent as a Lie module over H. Mathlib actually contains the following slightly more general result which holds for any Noetherian Lie module M [src]: instance [lie_algebra.is_nilpotent R L] [is_noetherian R L] [is_noetherian R M] : is_nilpotent R L $ weight_space M (0 : L → R) := Once we know that L is nilpotent over H, the self-normalizing property of a Cartan subalgebra ensures that H cannot be a strict submodule and the result is immediate. 123 Engel’s Theorem in Mathlib Page 9 of 10 18 6 Conclusion Having extolled the virtues of generality and unity, we should emphasise that in some sense they are two sides of the same coin. For example, the theory of root spaces discussed here depends on Mathlib’s theory of eigenspaces. This same theory of eigenspaces is also used in Mathlib’s library of functional analysis [3]. This is only possible because the theory of eigenspaces was developed quite generally (before either application existed). We thus enjoy a synergy: any lemma added by one consumer of the eigenspace theory is automatically available to the other. Although we have stated the required ﬁniteness condition for Engel’s theorem as the requirement that L be Noetherian as an R module, the argument actually needs only the weaker condition that the lattice of Lie subalgebras of L possesses a maximality property. Our version of Engel’s theorem seems not to exist in the literature. One notable close pass is an old paper of Zorn [10] where the result is proved for Lie rings (but not for their Lie modules). Another interesting paper is Jacobson [5]. In place of our: L ⊆ End(M ), he proves Engel’s theorem for what he calls a -subring: A ⊆ U. On the one hand Jacobson’s result is more general since the class of -subrings includes Lie subrings of associative rings as a special case. On the other hand it is less general since he obtains his result subject to the much more restrictive assumption that the lattice of ideals of the enclosing ring U possesses a minimality condition whereas we require only that the lattice of subalgebras of L possesses a maximality condition. Finally we should mention that there is an important setting where Engel-type results for Lie rings play a central role. See for example Zel’manov’s breakthrough [9]. Acknowledgements I am grateful to Kevin Buzzard at Imperial College whose Excellence Fund in Frontier Research grant funded this work. I am also grateful to the anonymous referees for numerous helpful remarks. I declare that this article is the sole work of the named author and that I have no conﬂicts of interest pertaining to any of the work discussed here. All code is available in the master branch of the open-source Mathlib repository, with links appearing throughout the text. Author Contributions The single author of this manuscript is responsible for all of the work. Declarations Competing Interests The authors declare no competing interests. Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/. I.e., any non-empty subset of Lie subalgebras contains a maximal element. 123 18 Page 10 of 10 O. Nash References 1. Bourbaki, N.: Lie Groups and Lie Algebras. Chapters 1–3. Elements of Mathematics (Berlin), p. 450. Springer, New York (1998). Translated from the French, Reprint of the 1989 English translation 2. Carneiro, M.: The type theory of lean. Master thesis (2019) 3. Dupuis, F., Lewis, R.Y., Macbeth, H.: Formalized functional analysis with semilinear maps. In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7–10, 2022, Haifa, OR, Israel (2022). arXiv:2202.05360 4. Fulton, W., Harris, J.: Representation Theory. Graduate Texts in Mathematics, vol. 129, p. 551. Springer, New York (1991). https://doi.org/10.1007/978-1-4612-0979-9. A ﬁrst course, Readings in Mathematics 5. Jacobson, N.: Une généralisation du théorème d’Engel. C. R. Acad. Sci. Paris 234, 579–581 (1952) 6. Nash, O.: Formalising Lie Algebras. Association for Computing Machinery, New York, NY, USA (2022). https://doi.org/10.1145/3497775.3503672 7. Serre, J.-P.: Complex Semisimple Lie Algebras, p. 74. Springer, New York (1987). https://doi.org/10. 1007/978-1-4757-3910-7 . Translated from the French by G. A. Jones 8. The mathlib community: The Lean mathematical library. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certiﬁed Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20–21, 2020, pp. 367–381 (2020). https://doi.org/10.1145/3372885.3373824 9. Zel’manov, E.I.: Solution of the restricted Burnside problem for groups of odd exponent. Izv. Akad. Nauk SSSR Ser. Mat. 54(1), 42–59221 (1990) 10. Zorn, M.: On a theorem of Engel. Bull. Am. Math. Soc. 43(6), 401–404 (1937). https://doi.org/10.1090/ S0002-9904-1937-06565-7 Publisher’s Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional afﬁliations.
Journal of Automated Reasoning – Springer Journals
Published: Jun 1, 2023
Keywords: Lean; Proof assistant; Formal math; Lie algebra; Nilpotency; Engel’s theorem; Root space; 17B30; 68V15; 68V20
You can share this free article with as many people as you like with the url below! We hope you enjoy this feature!
Read and print from thousands of top scholarly journals.
Already have an account? Log in
Bookmark this article. You can see your Bookmarks on your DeepDyve Library.
To save an article, log in first, or sign up for a DeepDyve account if you don’t already have one.
Copy and paste the desired citation format or use the link below to download a file formatted for EndNote
Access the full text.
Sign up today, get DeepDyve free for 14 days.
All DeepDyve websites use cookies to improve your online experience. They were placed on your computer when you launched this website. You can change your cookie settings through your browser.