In the intro to chapter 6, I feel like it would be a good idea to give an example of why/when we would use things like points, vectors, vectors acting on points, scalars multiplied by scalars, etc for real-world applications, like robotics or something
Also, I think it would be nice to put into the introduction of chapter 6 why we are focusing on algebraic structures, and how we are planning on using what we learned in chapters 1-5 in chapter 6. I thought this because it seemed like CH 6 is the final chapter that ties everything together
6.1.1. Extended Example
"The symetries are rotations that leave the rotated triangle sitting right on top of where it was in its unrotated state."
Should be "The symmetries are rotations that leave the rotated triangle sitting right on top of where it was in its unrotated state."
"Finally we need our set of elements to includes an identity element, e, that when composed with any element, r, just yields r."
Should be "Finally we need our set of elements to include an identity element, e, that when composed with any element, r, just yields r."
6.1.3. Monoid Typeclass
"Once we do that, we’ll benefit from all of the machinery (including notations and other operations) that come Lean’s monoid and its underlying typeclass definitions."
Should be ". Once we do that, we’ll benefit from all of the machinery (including notations and other operations) that come with Lean’s monoid and its underlying typeclass definitions."
"So Let’s see what we need for those, digging down until we reach simplest typeclasses."
Should be "So let’s see what we need for those, digging down until we reach simplest typeclasses."
6.1.4. Semigroup
"We see that to define a semigroup instance we’ll need an instance of has_mul, so let’s look at that. TEXT."
Need to get rid of the "TEXT" at the end.
6.1.8. mul_one_class instance
"We aready have an instance of has_mul, so all we need to define now is has_one, which identities the identity element in the monoid, which will then be denoted by 1."
Should be "We already have an instance of has_mul, so all we need to define now is has_one, which identities the identity element in the monoid, which will then be denoted by 1."
6.2.1.3. Chapter plan
"In the rest of this chapter, we’ll work out an extended example of a formal specification of, and of computation involving, a small, discrete, finite group, namely the group of rotational symmetries of an equilateral triangle,"
Should be a period at the end, not a comma.
"A rotation of this kind rotates an equilateral triangle by an amount that makes the resulting triang sit right on top of the original equilateral triangle."
Should be "A rotation of this kind rotates an equilateral triangle by an amount that makes the resulting triangle sit right on top of the original equilateral triangle."
6.2.2.2. Monoid
"As something of a detailed design detail, In Lean, the group class doesn’t extend from monoid directly."
Should be "As something of a detailed design detail, in Lean, the group class doesn’t extend from monoid directly."
6.2.2.3. div_inv_monoid
", implements a⁻¹ inverse operation"
There is this part of a sentence beginning after the bullet list that looks out of place.
6.3 Actions
"We now seen that group elements can be understood as actions that can be performed on some other kinds of objects. "
Should be something like "We have now seen that group elements can be understood as actions that can be performed on some other kinds of objects. "
6.3.2. Typeclasses
"To instantiate the group_action typeclass, we’ll have to do so for the group_smul class, providing an implementation of the smul function that computes the results of group actions; and we’ll have to gven proofs of compliance with the two axioms."
Should be "To instantiate the group_action typeclass, we’ll have to do so for the group_smul class, providing an implementation of the smul function that computes the results of group actions; and we’ll have to give proofs of compliance with the two axioms."
6.4.2. Readings
Maybe include readings before the introduction for better understanding at the start of this section?
6.4.4.1. add_monoid rot
"To structure rot as an additive group, we need first to structure it as as additive monoid."
Should be "To structure rot as an additive group, we need first to structure it as an additive monoid."
6.4.4.2. add_group rot
"Next we formulate the action of a rotation on a triange."
Should be "Next we formulate the action of a rotation on a triangle."
6.5. Modules
"We’ve now undertood what it means to be a torsor over a group."
Should be "We’ve now understood what it means to be a torsor over a group. "
"That fact that rotational symmetries form an additive group lets us do additive group math on symmetries: associative add, additively invert, subtract, zero left/right identity."
Should be "The fact that rotational symmetries form an additive group lets us do additive group math on symmetries: associative add, additively invert, subtract, zero left/right identity."
"If sclars have multiplicative inverses as well, and thus division, then you have a scalar field. "
Should be "If scalars have multiplicative inverses as well, and thus division, then you have a scalar field. "
6.5.3.1. Module
"Now we can make sense of the module typeclass instance constructor. You can see where each value below slots into the structure. The ℤ and rot type arguments will be implicit, along with the required typeclass instances We will then give the two new proof values explicitly."
Should be "Now we can make sense of the module typeclass instance constructor. You can see where each value below slots into the structure. The ℤ and rot type arguments will be implicit, along with the required typeclass instances. We will then give the two new proof values explicitly."
6.5.4.2. distrib_mul_action Z rot
"In other workds,"
Should be "In other words,"
"The we’ll need to prove that scaling a rotation b by scalar (x y) is the same as scalaing b first by y then by x."
Should be "Then we’ll need to prove that scaling a rotation b by scalar (x y) is the same as scaling b first by y then by x."
"With our (mul_action ℤ rot) defined we now put together the final peices needed for (distrib_mul_action ℤ rot)."
Should be "With our (mul_action ℤ rot) defined we now put together the final pieces needed for (distrib_mul_action ℤ rot)."
6.6. Vector Spaces
"That roughly mean that there will be multiplicative inverses of scalars, so fractions; and so all fractions of actions will also have to be actions."
Should be "That roughly means that there will be multiplicative inverses of scalars, so fractions; and so all fractions of actions will also have to be actions."
6.6.2. Torsor over vector space
"Formlizing ℚ as a torsor over itself as a vector space is straightforward, requiring only proofs of the two torsor laws, where the values are all rationals."
Should be "Formalizing ℚ as a torsor over itself as a vector space is straightforward, requiring only proofs of the two torsor laws, where the values are all rationals."
"We can now at least signal our abstract intent by using operations that reflect our intended interpretations of their argment as points, vectors, or scalars. "
Should be "We can now at least signal our abstract intent by using operations that reflect our intended interpretations of their argument as points, vectors, or scalars. "
6.7. Affine Spaces
"Vectors in our 3-dgeometric space represent displacements: differences between points in space."
Should be "Vectors in our 3-d geometric space represent displacements: differences between points in space."
"In this chapter we’ll formalize these abstractions and show how to enforce the requisite type distinctions between points and vectors. while inheriting a full affine space structure on these new types."
Should be "In this chapter we’ll formalize these abstractions and show how to enforce the requisite type distinctions between points and vectors while inheriting a full affine space structure on these new types."
6.7.1. Introduction
"To see what can go wrong, suppose p is a point representedby the rational 1/2 and v is a vector, literally a rational, namely 1/4. "
Should be "To see what can go wrong, suppose p is a point represented by the rational 1/2 and v is a vector, literally a rational, namely 1/4. "
6.7.2. Example
"The conclusion is that while we might want to represent abstract points and vectors as rational numbers, we don’t want to treat them rationals."
Should be something like "The conclusion is that while we might want to represent abstract points and vectors as rational numbers, we don’t want to treat them as rational."
6.7.3.2. Vectors
"Given that differences between points still have the type of bare rationals, we can use our vector object whereever any rational is expected, and we can use any rational, no matter what it actually means, as a vector in our physical and geometric computations."
Should be "Given that differences between points still have the type of bare rationals, we can use our vector object wherever any rational is expected, and we can use any rational, no matter what it actually means, as a vector in our physical and geometric computations."
In the intro to chapter 6, I feel like it would be a good idea to give an example of why/when we would use things like points, vectors, vectors acting on points, scalars multiplied by scalars, etc for real-world applications, like robotics or something
Also, I think it would be nice to put into the introduction of chapter 6 why we are focusing on algebraic structures, and how we are planning on using what we learned in chapters 1-5 in chapter 6. I thought this because it seemed like CH 6 is the final chapter that ties everything together
6.1.1. Extended Example "The symetries are rotations that leave the rotated triangle sitting right on top of where it was in its unrotated state." Should be "The symmetries are rotations that leave the rotated triangle sitting right on top of where it was in its unrotated state."
"Finally we need our set of elements to includes an identity element, e, that when composed with any element, r, just yields r." Should be "Finally we need our set of elements to include an identity element, e, that when composed with any element, r, just yields r."
6.1.3. Monoid Typeclass "Once we do that, we’ll benefit from all of the machinery (including notations and other operations) that come Lean’s monoid and its underlying typeclass definitions." Should be ". Once we do that, we’ll benefit from all of the machinery (including notations and other operations) that come with Lean’s monoid and its underlying typeclass definitions."
"So Let’s see what we need for those, digging down until we reach simplest typeclasses." Should be "So let’s see what we need for those, digging down until we reach simplest typeclasses."
6.1.4. Semigroup "We see that to define a semigroup instance we’ll need an instance of has_mul, so let’s look at that. TEXT." Need to get rid of the "TEXT" at the end.
6.1.8. mul_one_class instance "We aready have an instance of has_mul, so all we need to define now is has_one, which identities the identity element in the monoid, which will then be denoted by 1." Should be "We already have an instance of has_mul, so all we need to define now is has_one, which identities the identity element in the monoid, which will then be denoted by 1."
6.2.1.3. Chapter plan "In the rest of this chapter, we’ll work out an extended example of a formal specification of, and of computation involving, a small, discrete, finite group, namely the group of rotational symmetries of an equilateral triangle," Should be a period at the end, not a comma.
"A rotation of this kind rotates an equilateral triangle by an amount that makes the resulting triang sit right on top of the original equilateral triangle."
Should be "A rotation of this kind rotates an equilateral triangle by an amount that makes the resulting triangle sit right on top of the original equilateral triangle."
6.2.2.2. Monoid "As something of a detailed design detail, In Lean, the group class doesn’t extend from monoid directly." Should be "As something of a detailed design detail, in Lean, the group class doesn’t extend from monoid directly."
6.2.2.3. div_inv_monoid ", implements a⁻¹ inverse operation" There is this part of a sentence beginning after the bullet list that looks out of place.
6.3 Actions "We now seen that group elements can be understood as actions that can be performed on some other kinds of objects. " Should be something like "We have now seen that group elements can be understood as actions that can be performed on some other kinds of objects. "
6.3.2. Typeclasses "To instantiate the group_action typeclass, we’ll have to do so for the group_smul class, providing an implementation of the smul function that computes the results of group actions; and we’ll have to gven proofs of compliance with the two axioms." Should be "To instantiate the group_action typeclass, we’ll have to do so for the group_smul class, providing an implementation of the smul function that computes the results of group actions; and we’ll have to give proofs of compliance with the two axioms."
6.4.2. Readings Maybe include readings before the introduction for better understanding at the start of this section?
6.4.4.1. add_monoid rot "To structure rot as an additive group, we need first to structure it as as additive monoid." Should be "To structure rot as an additive group, we need first to structure it as an additive monoid."
6.4.4.2. add_group rot "Next we formulate the action of a rotation on a triange." Should be "Next we formulate the action of a rotation on a triangle."
6.5. Modules "We’ve now undertood what it means to be a torsor over a group." Should be "We’ve now understood what it means to be a torsor over a group. "
"That fact that rotational symmetries form an additive group lets us do additive group math on symmetries: associative add, additively invert, subtract, zero left/right identity." Should be "The fact that rotational symmetries form an additive group lets us do additive group math on symmetries: associative add, additively invert, subtract, zero left/right identity."
"If sclars have multiplicative inverses as well, and thus division, then you have a scalar field. " Should be "If scalars have multiplicative inverses as well, and thus division, then you have a scalar field. "
6.5.3.1. Module "Now we can make sense of the module typeclass instance constructor. You can see where each value below slots into the structure. The ℤ and rot type arguments will be implicit, along with the required typeclass instances We will then give the two new proof values explicitly." Should be "Now we can make sense of the module typeclass instance constructor. You can see where each value below slots into the structure. The ℤ and rot type arguments will be implicit, along with the required typeclass instances. We will then give the two new proof values explicitly."
6.5.4.2. distrib_mul_action Z rot "In other workds," Should be "In other words,"
"The we’ll need to prove that scaling a rotation b by scalar (x y) is the same as scalaing b first by y then by x." Should be "Then we’ll need to prove that scaling a rotation b by scalar (x y) is the same as scaling b first by y then by x."
"With our (mul_action ℤ rot) defined we now put together the final peices needed for (distrib_mul_action ℤ rot)." Should be "With our (mul_action ℤ rot) defined we now put together the final pieces needed for (distrib_mul_action ℤ rot)."
6.6. Vector Spaces "That roughly mean that there will be multiplicative inverses of scalars, so fractions; and so all fractions of actions will also have to be actions." Should be "That roughly means that there will be multiplicative inverses of scalars, so fractions; and so all fractions of actions will also have to be actions."
6.6.2. Torsor over vector space "Formlizing ℚ as a torsor over itself as a vector space is straightforward, requiring only proofs of the two torsor laws, where the values are all rationals." Should be "Formalizing ℚ as a torsor over itself as a vector space is straightforward, requiring only proofs of the two torsor laws, where the values are all rationals."
"We can now at least signal our abstract intent by using operations that reflect our intended interpretations of their argment as points, vectors, or scalars. " Should be "We can now at least signal our abstract intent by using operations that reflect our intended interpretations of their argument as points, vectors, or scalars. "
6.7. Affine Spaces "Vectors in our 3-dgeometric space represent displacements: differences between points in space." Should be "Vectors in our 3-d geometric space represent displacements: differences between points in space."
"In this chapter we’ll formalize these abstractions and show how to enforce the requisite type distinctions between points and vectors. while inheriting a full affine space structure on these new types." Should be "In this chapter we’ll formalize these abstractions and show how to enforce the requisite type distinctions between points and vectors while inheriting a full affine space structure on these new types."
6.7.1. Introduction "To see what can go wrong, suppose p is a point representedby the rational 1/2 and v is a vector, literally a rational, namely 1/4. " Should be "To see what can go wrong, suppose p is a point represented by the rational 1/2 and v is a vector, literally a rational, namely 1/4. "
6.7.2. Example "The conclusion is that while we might want to represent abstract points and vectors as rational numbers, we don’t want to treat them rationals." Should be something like "The conclusion is that while we might want to represent abstract points and vectors as rational numbers, we don’t want to treat them as rational."
6.7.3.2. Vectors "Given that differences between points still have the type of bare rationals, we can use our vector object whereever any rational is expected, and we can use any rational, no matter what it actually means, as a vector in our physical and geometric computations." Should be "Given that differences between points still have the type of bare rationals, we can use our vector object wherever any rational is expected, and we can use any rational, no matter what it actually means, as a vector in our physical and geometric computations."