diff --git a/.vscode/settings.json b/.vscode/settings.json index bec94634..89e9ffc6 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -18,5 +18,22 @@ "cSpell.words": [ "monoids", "numref" - ] + ], + "spellright.language": [ + "en_US" + ], + "spellright.documentTypes": [ + "markdown", + "latex", + "plaintext", + "lean4" + ], + "spellright.parserByClass": { + "lean4": { + "parser": "code", + "comment_start": "/-", + "comment_end": "-/", + "comment_line": "--" + } + } } diff --git a/MIL.lean b/MIL.lean index 69660c0e..e6309a1d 100644 --- a/MIL.lean +++ b/MIL.lean @@ -24,6 +24,7 @@ import MIL.C07_Hierarchies.S01_Basics import MIL.C07_Hierarchies.S02_Morphisms import MIL.C07_Hierarchies.S03_Subobjects import MIL.C08_Groups_and_Rings.S01_Groups +import MIL.C08_Groups_and_Rings.S02_Rings import MIL.C10_Topology.S01_Filters import MIL.C10_Topology.S02_Metric_Spaces import MIL.C10_Topology.S03_Topological_Spaces diff --git a/MIL/C08_Groups_and_Rings/S01_Groups.lean b/MIL/C08_Groups_and_Rings/S01_Groups.lean index e8168796..227842a0 100644 --- a/MIL/C08_Groups_and_Rings/S01_Groups.lean +++ b/MIL/C08_Groups_and_Rings/S01_Groups.lean @@ -1,10 +1,9 @@ -- BOTH: -import Mathlib.Algebra.Ring.Defs -import Mathlib.Data.Real.Basic import Mathlib.GroupTheory.Sylow import Mathlib.GroupTheory.Perm.Cycle.Concrete import Mathlib.GroupTheory.Perm.Subgroup import Mathlib.GroupTheory.PresentedGroup + import MIL.Common /- TEXT: @@ -66,7 +65,7 @@ f.map_zero -- QUOTE. /- TEXT: -Those morphisms are bundled maps, ie they package together a map and some properties of this map. +Those morphisms are bundled maps, ie. they package together a map and some properties of this map. :numref:`section_hierarchies_morphisms` contain a lot more explanations about that. Here we simply note the slightly unfortunate consequence that we cannot use ordinary function composition. We need to use ``MonoidHom.comp`` and ``AddMonoidHom.comp``. @@ -164,6 +163,17 @@ example {G H : Type*} [Group G] [Group H] (f : G ≃* H) : f.trans f.symm = MulEquiv.refl G := f.self_trans_symm +-- QUOTE. +/- TEXT: +One can use ``MulEquiv.ofBijective`` to build an isomorphism from a bijective morphism. +Of course this results in non computable inverse functions. +EXAMPLES: -/ +-- QUOTE: + +noncomputable example {G H : Type*} [Group G] [Group H] (f : G →* H) (h : Function.Bijective f) : + G ≃* H := + MulEquiv.ofBijective f h + -- QUOTE. /- TEXT: Subgroups @@ -188,6 +198,9 @@ But it is endowed with a coercion to ``Set G`` and a membership predicate on ``G See :numref:`section_hierarchies_subobjects` for explanations about why and how things are set up like this. +Of course two subgroups are the same if and only if they have the same elements, and this fact +is registered for use with the ``ext`` tactic, just like for bare sets. + If you want how to state and prove something like ``ℤ`` is an additive subgroup of ``ℚ`` then the answer to constructor a term with type ``AddSubgroup ℚ`` whose projection to ``Set ℚ`` is ``ℤ``, or more precisely the image of ``ℤ`` in ``ℚ``. @@ -255,7 +268,7 @@ EXAMPLES: -/ example {G : Type*} [Group G] (H H' : Subgroup G) : ((H ⊔ H' : Subgroup G) : Set G) = Subgroup.closure ((H : Set G) ∪ (H' : Set G)) := by - simp [Subgroup.closure_union, Subgroup.closure_eq] + rw [Subgroup.sup_eq_closure] -- QUOTE. /- TEXT: @@ -275,6 +288,47 @@ EXAMPLES: -/ example {G : Type*} [Group G] (x : G) : x ∈ (⊥ : Subgroup G) ↔ x = 1 := Subgroup.mem_bot +-- QUOTE. +/- TEXT: +As an exercise in manipulating groups and subgroups, you can define the conjuguate of a subgroup +by an element of the ambiant group. +EXAMPLES: -/ +-- QUOTE: + +def conjugate {G : Type*} [Group G] (x : G) (H : Subgroup G) : Subgroup G where + carrier := {a : G | ∃ h, h ∈ H ∧ a = x * h * x⁻¹} + one_mem' := by +/- EXAMPLES: + dsimp + sorry +SOLUTIONS: -/ + dsimp + use 1 + constructor + exact H.one_mem + group +-- BOTH: + inv_mem' := by +/- EXAMPLES: + dsimp + sorry +SOLUTIONS: -/ + dsimp + rintro - ⟨h, h_in, rfl⟩ + use h⁻¹, H.inv_mem h_in + group +-- BOTH: + mul_mem' := by +/- EXAMPLES: + dsimp + sorry +SOLUTIONS: -/ + dsimp + rintro - - ⟨h, h_in, rfl⟩ ⟨k, k_in, rfl⟩ + use h*k, H.mul_mem h_in k_in + group +-- BOTH: + -- QUOTE. /- TEXT: Tying the previous two topics together, one can push forward and pull back subgroups using @@ -288,6 +342,9 @@ Subgroup.map f G' example {G H : Type*} [Group G] [Group H] (H' : Subgroup H) (f : G →* H) : Subgroup G := Subgroup.comap f H' + +#check Subgroup.mem_map +#check Subgroup.mem_comap -- QUOTE. /- TEXT: @@ -307,9 +364,78 @@ example {G H : Type*} [Group G] [Group H] (f : G →* H) (h : H) : -- QUOTE. /- TEXT: -Let us finish this introduction to subgroups in Mathlib with two very useful results. +As exercises in manipulating group morphisms and subgroups, let us prove some elementary properties. +Of course they are already in Mathlib so do not use ``exact?`` too early if you want to benefit +from those exercises. +EXAMPLES: -/ +-- QUOTE: +section exercises +variable {G H : Type*} [Group G] [Group H] + +open Subgroup + +example (φ : G →* H) (S T : Subgroup H) (hST : S ≤ T) : comap φ S ≤ comap φ T :=by +/- EXAMPLES: + sorry +SOLUTIONS: -/ + intro x hx + rw [mem_comap] at * -- Lean does not need this line + exact hST hx + +-- BOTH: + +example (φ : G →* H) (S T : Subgroup G) (hST : S ≤ T) : map φ S ≤ map φ T :=by +/- EXAMPLES: + sorry +SOLUTIONS: -/ + intro x hx + rw [mem_map] at * -- Lean does not need this line + rcases hx with ⟨y, hy, rfl⟩ + use y, hST hy +-- BOTH: + +variable {K : Type*} [Group K] + +-- Remember you can use the `ext` tactic to prove an equality of subgroups. +example (φ : G →* H) (ψ : H →* K) (U : Subgroup K) : + comap (ψ.comp φ) U = comap φ (comap ψ U) := by +/- EXAMPLES: + sorry +SOLUTIONS: -/ + -- The whole proof could be ``rfl``, but let's decompose it a bit. + ext x + simp only [mem_comap] + rfl +-- BOTH: + +-- Pushing a Subgroup along one homomorphism and then another is equal to +-- pushing it forward along the composite of the homomorphisms. +example (φ : G →* H) (ψ : H →* K) (S : Subgroup G) : + map (ψ.comp φ) S = map ψ (S.map φ) := by +/- EXAMPLES: + sorry +SOLUTIONS: -/ + ext x + simp only [mem_map] + constructor + · rintro ⟨y, y_in, hy⟩ + exact ⟨φ y, ⟨y, y_in, rfl⟩, hy⟩ + · rintro ⟨y, ⟨z, z_in, hz⟩, hy⟩ + use z, z_in + calc ψ.comp φ z = ψ (φ z) := rfl + _ = ψ y := by congr + _ = x := hy +-- BOTH: +end exercises +-- QUOTE. + +/- TEXT: +Let us finish this introduction to subgroups in Mathlib with two very classical results. Lagrange theorem states the cardinal of a subgroup of a finite group divides the cardinal of the group. Sylow's first theorem is a very famous partial converse to Lagrange's theorem. + +Since this corner of Mathlib is partly setup to allow actual computations, we need to tell +Lean to use non-constructive logic using the following ``attribute`` command. EXAMPLES: -/ -- QUOTE: @@ -326,6 +452,40 @@ example {G : Type*} [Group G] [Fintype G] (p : ℕ) {n : ℕ} [Fact p.Prime] (hdvd : p ^ n ∣ card G) : ∃ K : Subgroup G, card K = p ^ n := Sylow.exists_subgroup_card_pow_prime p hdvd +-- QUOTE. + +/- TEXT: +The next two exercises derive a corollary of Lagrange's lemma (which is already in Mathlib, +so do not use `exact?` too early). +EXAMPLES: -/ +-- QUOTE: + + +lemma eq_bot_iff_card {G : Type*} [Group G] {H : Subgroup G} [Fintype H] : H = ⊥ ↔ card H = 1 := by + suffices (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x by + simpa [eq_bot_iff_forall, card_eq_one_iff] +/- EXAMPLES: + sorry +SOLUTIONS: -/ + constructor + · intro h + use 1, H.one_mem + · rintro ⟨y, -, hy'⟩ x hx + calc x = y := hy' x hx + _ = 1 := (hy' 1 H.one_mem).symm + +-- BOTH: +#check card_dvd_of_le + +lemma inf_bot_of_coprime {G : Type*} [Group G] (H K : Subgroup G) [Fintype H] [Fintype K] + (h : (card H).Coprime (card K)) : H ⊓ K = ⊥ := by +/- EXAMPLES: + sorry +SOLUTIONS: -/ + have D₁ : card (H ⊓ K : Subgroup G) ∣ card H := card_dvd_of_le inf_le_left + have D₂ : card (H ⊓ K : Subgroup G) ∣ card K := card_dvd_of_le inf_le_right + exact eq_bot_iff_card.2 (Nat.eq_one_of_dvd_coprimes h D₁ D₂) + -- QUOTE. /- TEXT: Concrete groups @@ -435,7 +595,7 @@ An action of a group ``G`` on some type ``X`` is nothing but a morphism from ``G But we don't want to carry around this morphism everywhere, we want it to be automatically inferred by Lean as much as possible. So we have a type class for this, which is ``MulAction G X``. The downside of this setup is that having multiple actions of the same group on the same type -requires some contorsions, such as defining type synonyms carrying different instances. +requires some contortions, such as defining type synonyms carrying different instances. This setup allows in particular to use ``g • x`` to denote the action of a group element ``g`` on a point ``x``. @@ -540,8 +700,46 @@ example {G : Type*} [Group G] (H : Subgroup G) : G ≃ (G ⧸ H) × H := /- TEXT: which is the conceptual version of Lagrange theorem that we saw above. Note this version makes no finiteness assumption. + +As an exercise for this section, let us build the action of a group on its subgroup by +conjugation, using our definition ``conjugate`` from a previous exercise. EXAMPLES: -/ -- QUOTE: +variable {G : Type*} [Group G] + +lemma conjugate_one (H : Subgroup G) : conjugate 1 H = H := by +/- EXAMPLES: + sorry +SOLUTIONS: -/ + ext x + simp [conjugate] +-- BOTH: + +instance : MulAction G (Subgroup G) where + smul := conjugate + one_smul := by +/- EXAMPLES: + sorry +SOLUTIONS: -/ + exact conjugate_one +-- BOTH: + mul_smul := by +/- EXAMPLES: + sorry +SOLUTIONS: -/ + intro x y H + ext z + constructor + · rintro ⟨h, h_in, rfl⟩ + use y*h*y⁻¹ + constructor + · use h + · group + · rintro ⟨-, ⟨h, h_in, rfl⟩, rfl⟩ + use h, h_in + group +-- BOTH: + end GroupActions @@ -608,18 +806,134 @@ example {G G': Type*} [Group G] [Group G'] {N : Subgroup G} [N.Normal] {N' : Subgroup G'} [N'.Normal] {φ : G →* G'} (h : N ≤ Subgroup.comap φ N') : G ⧸ N →* G'⧸ N':= QuotientGroup.map N N' φ h +-- QUOTE. -/- +/- TEXT: One subtle point to understand is that the type ``G ⧸ N`` really depends on ``N`` (up to definitional equality), so having a proof that two normal subgroups ``N`` and ``M`` are equal is not enough to make the corresponding quotients equal. However the universal properties does give an isomorphism in this case. --/ +EXAMPLES: -/ +-- QUOTE: example {G : Type*} [Group G] {M N : Subgroup G} [M.Normal] [N.Normal] (h : M = N) : G ⧸ M ≃* G ⧸ N := QuotientGroup.quotientMulEquivOfEq h +-- QUOTE. + +/- TEXT: + +As a final series of exercises for this section, we will prove that if ``H`` and ``K`` are disjoint +normal subgroups of a finite group ``G`` whose cardinals have product the cardinal of ``G`` +then ``G`` is isomorphic to ``H × K``. Recall that disjoint in this context means ``H ⊓ K = ⊥``. + +We start with playing a bit with Lagrange's lemma, without assuming the subgroups are normal +or disjoint. +EXAMPLES: -/ +-- QUOTE: + +section +variable {G : Type*} [Group G] {H K : Subgroup G} + +open MonoidHom + +#check card_pos -- The nonempty argument will be automatically inferred for subgroups +#check Subgroup.index_eq_card +#check Subgroup.index_mul_card +#check Nat.eq_of_mul_eq_mul_right + +lemma aux_card_eq [Fintype G] (h' : card G = card H * card K) : card (G⧸H) = card K := by +/- EXAMPLES: + sorry +SOLUTIONS: -/ + have := calc + card (G ⧸ H) * card H = card G := by rw [← H.index_eq_card, H.index_mul_card] + _ = card K * card H := by rw [h', mul_comm] + + exact Nat.eq_of_mul_eq_mul_right card_pos this +-- QUOTE. + +/- TEXT: +From now on, we assume our subgroup are normal and disjoint, and the cardinality condition. + +We construct the first building block of the desired isomorphism. + +EXAMPLES: -/ +-- QUOTE: + +variable [H.Normal] [K.Normal] [Fintype G] (h : Disjoint H K) (h' : card G = card H * card K) + + +#check bijective_iff_injective_and_card +#check ker_eq_bot_iff +#check restrict +#check ker_restrict + + +def iso₁ [Fintype G] (h : Disjoint H K) (h' : card G = card H * card K) : K ≃* G⧸H := by +/- EXAMPLES: + sorry +SOLUTIONS: -/ + apply MulEquiv.ofBijective ((QuotientGroup.mk' H).restrict K) + rw [bijective_iff_injective_and_card] + constructor + · rw [← ker_eq_bot_iff, (QuotientGroup.mk' H).ker_restrict K] + simp [h] + · symm + exact aux_card_eq h' + +-- QUOTE. + +/- TEXT: + +Next we will need ``MonoidHom.prod`` which builds a morphism from ``G₀`` to ``G₁ × G₂`` out of +morphisms from ``G₀`` to ``G₁`` and ``G₂``. + +The following lemma is currently missing from Mathlib. +EXAMPLES: -/ +-- QUOTE: + +#check MulHom.prod + +theorem MonoidHom.ker_prod {M N P : Type*} [Group M] [MulOneClass N] [MulOneClass P] + (f : M →* N) (g : M →* P) : ker (f.prod g) = ker f ⊓ ker g := by + ext x + simp [MonoidHom.mem_ker] + +-- QUOTE. + +/- TEXT: + +Now we can define our second building block. + +EXAMPLES: -/ +-- QUOTE: + +def iso₂ : G ≃* (G⧸K) × (G⧸H) := by +/- EXAMPLES: + sorry +SOLUTIONS: -/ + apply MulEquiv.ofBijective <| (QuotientGroup.mk' K).prod (QuotientGroup.mk' H) + rw [bijective_iff_injective_and_card] + constructor + · rw [← ker_eq_bot_iff, ker_prod] + simp [h.symm.eq_bot] + · rw [card_prod, aux_card_eq h', aux_card_eq (mul_comm (card H) _▸ h'), h'] +-- QUOTE. + +/- TEXT: +We are ready to put all pieces together. +EXAMPLES: -/ +-- QUOTE: + +#check MulEquiv.prodCongr +def finalIso : G ≃* H × K := +/- EXAMPLES: + sorry +SOLUTIONS: -/ + (iso₂ h h').trans ((iso₁ h.symm (mul_comm (card H) _ ▸ h')).prodCongr (iso₁ h h')).symm +end end QuotientGroup -- QUOTE. diff --git a/MIL/C08_Groups_and_Rings/S02_Rings.lean b/MIL/C08_Groups_and_Rings/S02_Rings.lean index ab584672..60563261 100644 --- a/MIL/C08_Groups_and_Rings/S02_Rings.lean +++ b/MIL/C08_Groups_and_Rings/S02_Rings.lean @@ -11,8 +11,8 @@ noncomputable section /- TEXT: .. _rings: -Monoids and Groups ------------------- +Rings +----- .. index:: ring (algebraic structure) @@ -22,10 +22,12 @@ Rings, their units, morphisms and subrings The type of ring structures on a type ``R`` is ``Ring R``. The variant where multiplication is assumed to be commutative is ``CommRing R``. We already saw that the ``ring`` tactic will prove any equality that uses only the axioms of commutative rings. --/ +EXAMPLES: -/ +-- QUOTE: example {R : Type*} [CommRing R] (x y : R) : (x + y)^2 = x^2 + y^2 + 2*x*y := by ring -/- +-- QUOTE. +/- TEXT: More exotic variants do not ask that ``R`` equipped with addition form a group, but only an additive monoid. The corresponding type classes are ``Semiring R`` and ``CommSemiring R``. Arguably the most important motivation is to include natural numbers and related types such as @@ -33,11 +35,13 @@ functions taking values in natural number. The next important example is the type of ideals in a ring, which will be discussed below. In particular the name of the ``ring`` tactic is doubly misleading: it does assume commutativity but a ``CommSemiring`` is enough. --/ +EXAMPLES: -/ +-- QUOTE: example (x y : ℕ) : (x + y)^2 = x^2 + y^2 + 2*x*y := by ring -/- +-- QUOTE. +/- TEXT: There also versions that do not assume existence of a multiplicative unit or associativity of multiplication but we will not discuss those. @@ -57,7 +61,8 @@ This implementation detail is mostly relevant only when defining computable func situations one can use ``IsUnit.unit {x : M} : IsUnit x → Mˣ`` to build a unit. In the commutative case, one also has ``Units.mkOfMulEqOne (x y : M) : x * y = 1 → Mˣ`` which builds ``x`` seen as unit. --/ +EXAMPLES: -/ +-- QUOTE: example (x : ℤˣ) : x = 1 ∨ x = -1 := Int.units_eq_one_or x @@ -65,11 +70,13 @@ example {M : Type*} [Monoid M] {x : Mˣ} : (x : M)*x⁻¹ = 1 := Units.mul_inv x example {M : Type*} [Monoid M] : Group Mˣ := inferInstance -/- +-- QUOTE. +/- TEXT: The type of ring morphisms between two (semi)-rings ``R`` and ``S`` is ``RingHom R S``, with notation ``R →+* S``. --/ +EXAMPLES: -/ +-- QUOTE: example {R S : Type*} [Ring R] [Ring S] (f : R →+* S) (x y : R) : f (x + y) = f x + f y := f.map_add x y @@ -77,14 +84,17 @@ example {R S : Type*} [Ring R] [Ring S] (f : R →+* S) (x y : R) : example {R S : Type*} [Ring R] [Ring S] (f : R →+* S) : Rˣ →* Sˣ := Units.map f -/- +-- QUOTE. +/- TEXT: As with submonoids and subgroups, there is a ``Subring R`` type for subrings of a ring ``R``, but is a lot less useful than subgroups since those are not the right object to quotient by. --/ +EXAMPLES: -/ +-- QUOTE: example {R : Type*} [Ring R] (S : Subring R) : Ring S := inferInstance -/- +-- QUOTE. +/- TEXT: Also notice that ``RingHom.range`` produces a subring. Ideals and quotients @@ -99,49 +109,59 @@ safely ignored since most relevant lemmas are restated in the special context of However dot notation won't always work as expected. For instance one cannot replace ``Ideal.Quotient.mk I`` by ``I.Quotient.mk`` in the snippet below because the parser immediately replaces the ``Ideal R`` with ``Submodule R R``. --/ +EXAMPLES: -/ +-- QUOTE: example {R : Type*} [CommRing R] (I : Ideal R) : R →+* R⧸I := Ideal.Quotient.mk I -/- +-- QUOTE. +/- TEXT: The universal property of quotient rings is ``Ideal.Quotient.lift`` --/ +EXAMPLES: -/ +-- QUOTE: example {R S : Type*} [CommRing R] [CommRing S] (I : Ideal R) (f : R →+* S) (H : I ≤ RingHom.ker f) : R ⧸ I →+* S := Ideal.Quotient.lift I f H -/- +-- QUOTE. +/- TEXT: In particular it leads to the first isomorphism theorem for rings. --/ +EXAMPLES: -/ +-- QUOTE: example {R S : Type*} [CommRing R] [CommRing S](f : R →+* S) : R ⧸ RingHom.ker f ≃+* f.range := RingHom.quotientKerEquivRange f -/- +-- QUOTE. +/- TEXT: One can use ring morphisms to push or pull ideals using ``Ideal.map`` and ``Ideal.comap``. As usual, the later is more convenient to use since it does not involve an existential quantifier. This explains why it is used to state the condition allowing to build morphisms between quotient rings. --/ +EXAMPLES: -/ +-- QUOTE: example {R S : Type*} [CommRing R] [CommRing S] (I : Ideal R) (J : Ideal S) (f : R →+* S) (H : I ≤ Ideal.comap f J) : R ⧸ I →+* S ⧸ J := Ideal.quotientMap J f H - -/- +-- QUOTE. +/- TEXT: One subtle point to understand is that the type ``R ⧸ I`` really depends on ``I`` (up to definitional equality), so have a proof that two ideals ``I`` and ``J`` are equal is not enough to make the corresponding quotients equal. However the universal properties does give an isomorphism in this case. --/ +EXAMPLES: -/ +-- QUOTE: example {R : Type*} [CommRing R] {I J : Ideal R} (h : I = J) : R ⧸ I ≃+* R ⧸ J := Ideal.quotEquivOfEq h -/- +-- QUOTE. +/- TEXT: For instance we can now quote the Chinese remainder isomorphism. --/ +EXAMPLES: -/ +-- QUOTE: example {R : Type*} [CommRing R] {ι : Type*} [Fintype ι] (f : ι → Ideal R) (hf : ∀ i j, i ≠ j → IsCoprime (f i) (f j)) : (R ⧸ ⨅ i, f i) ≃+* Π i, R ⧸ f i := Ideal.quotientInfRingEquivPiQuotient f hf @@ -170,7 +190,8 @@ example {ι : Type*} [Fintype ι] (a : ι → ℕ) (coprime : ∀ i j, i ≠ j quotientInfRingEquivPiQuotient _ this |>.trans <| RingEquiv.piCongrRight fun i ↦ Int.quotientSpanNatEquivZMod (a i) -/- +-- QUOTE. +/- TEXT: Algebras and polynomials ^^^^^^^^^^^^^^^^^^^^^^^^ @@ -186,7 +207,8 @@ existence of more general notions of algebra whose definition is less concise. The fact that ``algebraMap R A`` is ring morphism packages a lot of properties of scalar multiplication, such as the following ones. --/ +EXAMPLES: -/ +-- QUOTE: example {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (r r' : R) (a : A) : (r + r') • a = r • a + r' • a := @@ -196,23 +218,22 @@ example {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (r r' : R) (a : A) : (r * r') • a = r • r' • a := mul_smul r r' a -/- +-- QUOTE. +/- TEXT: The morphisms of ``R`` algebras between two ``R``-algebras ``A`` and ``B`` are ring morphisms which commute with scalar multiplication by elements of ``R``. They are bundled morphism with type ``AlgHom R A B`` which is denoted by ``A →ₐ[R] B``. --/ -/- Very important examples of non-commutative algebras include endomorphisms algebra (or square matrices algebras), and those will be covered in the linear algebra chapter. In this chapter we will only discuss the most important commutative algebras: polynomials. - The algebra of univariate polynomials with coefficients in ``R`` is ``Polynomial R`` which is denoted by ``R[X]`` as soon as one opens the ``Polynomial`` namespace. The algebra structure map from ``R`` to ``R[X]`` is denoted by ``C``, which stands for "constant" since the corresponding polynomial functions are always constant. The indeterminate is denoted by ``X``. --/ +EXAMPLES: -/ +-- QUOTE: section Polynomials open Polynomial @@ -220,7 +241,9 @@ open Polynomial example {R : Type*} [CommRing R] : R[X] := X example {R : Type*} [CommRing R] (r : R) := X - C r -/- + +-- QUOTE. +/- TEXT: In the first example above, it is crucial that we give the expected type to Lean since it has no way to guess it from the body of the definition. In the second example, the target polynomial algebra can be inferred from our use of ``C r`` since the type of ``r`` is known. @@ -228,35 +251,25 @@ algebra can be inferred from our use of ``C r`` since the type of ``r`` is known Because ``C`` is a ring morphism from ``R`` to ``R[X]``, we can use all ring morphisms lemmas such as ``map_zero``, ``map_one``, ``map_mul``, ``map_pow`` before computing in the ring ``R[X]`` in the following example. --/ +EXAMPLES: -/ +-- QUOTE: example {R : Type*} [CommRing R] (r : R) : (X + C r) * (X - C r) = X^2 - C (r ^ 2) := by rw [C.map_pow] ring -/- +-- QUOTE. +/- TEXT: You can access coefficients using ``Polynomial.coeff`` --/ -example {R : Type*} [CommRing R](r:R) : (C r).coeff 0 = r := by exact coeff_C_zero - -section -variable {R : Type*} [Semiring R] -@[simp] -theorem coeff_ofNat_zero (a : ℕ) [a.AtLeastTwo] : coeff (no_index (OfNat.ofNat a : R[X])) 0 = (OfNat.ofNat a : R) := - coeff_monomial +EXAMPLES: -/ +-- QUOTE: -@[simp] -theorem coeff_ofNat_succ (a n : ℕ) [h : a.AtLeastTwo] : - coeff (no_index (OfNat.ofNat a : R[X])) (n + 1) = 0 := by - rw [← Nat.cast_eq_ofNat] - simp +example {R : Type*} [CommRing R](r:R) : (C r).coeff 0 = r := by simp -example {R : Type*} [CommRing R] : (X^2 + 2*X + C 3 : R[X]).coeff 1 = 2 := by - simp +example {R : Type*} [CommRing R] : (X^2 + 2*X + C 3 : R[X]).coeff 1 = 2 := by simp -end - -/- +-- QUOTE. +/- TEXT: Defining the degree of a polynomial is always tricky because of the special case of the zero polynomial. Mathlib has two variants: ``Polynomial.natDegree : R[X] → ℕ`` which assigns degree ``0`` to the zero polynomial, and ``Polynomial.degree : R[X] → WithBot ℕ`` where ``WithBot ℕ`` @@ -267,57 +280,66 @@ polynomial, and it is absorbant for addition (and almost for multiplication, exc The ``degree`` version is morally the correct one. For instance it allows to state the expected formula for the degree of a product (assuming the base ring has no zero divisor). --/ +EXAMPLES: -/ +-- QUOTE: example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} : degree (p * q) = degree p + degree q := Polynomial.degree_mul -/- +-- QUOTE. +/- TEXT: Whereas the version for ``natDegree`` needs to assume non-zero polynomials. --/ +EXAMPLES: -/ +-- QUOTE: example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} (hp : p ≠ 0) (hq : q ≠ 0) : natDegree (p * q) = natDegree p + natDegree q := Polynomial.natDegree_mul hp hq - -/- +-- QUOTE. +/- TEXT: However, ``ℕ`` is much nicer to use than ``WithBot ℕ``, hence both versions exists and there are lemmas to convert between them. Also ``natDegree`` is the correct definition to use when computing the degree of a composition. Composition of polynomial is ``Polynomial.comp`` and we have --/ - +EXAMPLES: -/ +-- QUOTE: example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} : natDegree (comp p q) = natDegree p * natDegree q := Polynomial.natDegree_comp -/- +-- QUOTE. +/- TEXT: Polynomial give rise to polynomial functions. In particular they can be evaluated on ``R`` using ``Poynomial.eval``. --/ +EXAMPLES: -/ +-- QUOTE: example {R : Type*} [CommRing R] (P: R[X]) (x : R) := P.eval x example {R : Type*} [CommRing R] (r : R) : (X - C r).eval r = 0 := by simp -/- +-- QUOTE. +/- TEXT: In particular there is ``IsRoot`` predicate that selects elements of ``r`` where a polynomial evaluation vanishes. --/ +EXAMPLES: -/ +-- QUOTE: example {R : Type*} [CommRing R] (P : R[X]) (r : R) : IsRoot P r ↔ P.eval r = 0 := Iff.rfl -/- +-- QUOTE. +/- TEXT: We would like to say that, assuming ``R`` has no zero divisor, a polynomial has at most as many roots, counted with multiplicities, as its degree. But again the case of the zero polynomial is painful. So Mathlib defines ``Polynomial.roots`` as sending a polynomial ``P`` to a multiset, ie a finite set with multiplicites defined to be empty if ``P`` is zero and its roots with multiplicities otherwise. This is defined only when the underlying ring is a domain since otherwise it has no good property. --/ +EXAMPLES: -/ +-- QUOTE: example {R : Type*} [CommRing R] [IsDomain R] (r : R) : (X - C r).roots = {r} := roots_X_sub_C r @@ -325,7 +347,8 @@ example {R : Type*} [CommRing R] [IsDomain R] (r : R) : (X - C r).roots = {r} := example {R : Type*} [CommRing R] [IsDomain R] (r : R) (n : ℕ): ((X - C r)^n).roots = n • {r} := by simp -/- +-- QUOTE. +/- TEXT: Both `Polynomial.eval` and `Polynomial.roots` consider only the coefficients ring. They do not allow to say that ``X^2 - 2 : ℚ[X]`` has a root in ``ℝ`` or that ``X^2 + 1 : ℝ[X]`` has a root in ``ℂ``. For this we need ``Polynomial.aeval`` which will evaluate ``P : R[X]`` in any ``R``-algebra. @@ -334,15 +357,18 @@ every element of ``a`` on the ``R``-algebra morphism of evaluation at ``a``. Sin has a coercion to functions, one can apply it to a polynomial. But ``aeval`` does not have a polynomial as an argument, so one cannot use dot notation like in ``P.eval`` above. --/ +EXAMPLES: -/ +-- QUOTE: example : aeval Complex.I (X^2 + 1 : ℝ[X]) = 0 := by simp -/- +-- QUOTE. +/- TEXT: The function corresponding to ``roots`` in this context is ``aroots`` which takes a polynomial and then an algebra and outputs a multiset (with the same caveat about the zero polynomial as for ``roots``). --/ +EXAMPLES: -/ +-- QUOTE: open Complex Polynomial example : aroots (X^2 + 1 : ℝ[X]) ℂ = {I, -I} := by @@ -357,19 +383,50 @@ example : aroots (X^2 + 1 : ℝ[X]) ℂ = {I, -I} := by simp only [factored, roots_mul p_ne_zero, roots_X_sub_C] rfl - -- Mathlib knows about D'Alembert-Gauss theorem: ``ℂ`` is algebraically closed. example : IsAlgClosed ℂ := inferInstance -/- +-- QUOTE. +/- TEXT: More generally, given an ring morphism ``f : R →+* S`` one can evaluate ``P : R[X]`` at a point in ``S`` using ``Polynomial.eval₂``. This one produces an actual function from ``R[X]`` to ``S`` since it does not assume the existence of a ``Algebra R S`` instance, so dot notation works as you would expect. --/ +EXAMPLES: -/ +-- QUOTE: #check (Complex.ofReal : ℝ →+* ℂ) example : (X^2 + 1 : ℝ[X]).eval₂ Complex.ofReal Complex.I = 0 := by simp +-- QUOTE. +/- TEXT: +Let us end by briefly mentioning multi-variate polynomials. Given a commutative semiring ``R``, +the ``R``-algebra of polynomial with coefficients in ``R`` and indeterminates indexed by +a type ``σ`` is ``MVPolynomial σ R``. Given ``i : σ``, the corresponding polynomial is +``MvPolynomial.X i`` (of course one can open the ``MVPolynomial`` namespace to shortent this +to ``X i``). +For instance, if we want two indeterminates we can use +``Fin 2`` as ``σ`` and write the polynomial defining the unit cicle in :math:`\mathbb{R}^2`` as: +EXAMPLES: -/ +-- QUOTE: + +open MvPolynomial + +def circleEquation : MvPolynomial (Fin 2) ℝ := X 0 ^ 2 + X 1 ^ 2 - 1 + +-- QUOTE. +/- TEXT: +Recall that function application has a very high precedence so the above equation is read as +``(X 0) ^ 2 + (X 1) ^ 2 - 1``. + +And we can evaluate it to make sure the point with coordinates :math:`(1, 0)` is on the circle. +Recall the ``![...]`` notation denotes elements of ``Fin n → X`` for some natural number ``n`` +determined by the number of arguments and some type ``X`` determined by the type of arguments. +EXAMPLES: -/ +-- QUOTE: + +example : MvPolynomial.eval ![0, 1] circleEquation = 0 := by simp [circleEquation] + end Polynomials +-- QUOTE. diff --git a/MIL/Common.lean b/MIL/Common.lean index 043f858a..272e7af7 100644 --- a/MIL/Common.lean +++ b/MIL/Common.lean @@ -1,4 +1,5 @@ import Mathlib.Tactic +import Mathlib.Util.PiNotation set_option warningAsError false @@ -6,37 +7,12 @@ namespace PiNotation open Lean.Parser Term open Lean.PrettyPrinter.Delaborator -/-- Dependent function type (a "pi type"). The notation `Π x : α, β x` can -also be written as `(x : α) → β x`. -/ --- A direct copy of forall notation but with `Π`/`Pi` instead of `∀`/`Forall`. -@[term_parser] -def piNotation := leading_parser:leadPrec - unicodeSymbol "Π" "Pi" >> - many1 (ppSpace >> (binderIdent <|> bracketedBinder)) >> - optType >> ", " >> termParser - -/-- Dependent function type (a "pi type"). The notation `Π x ∈ s, β x` is -short for `Π x, x ∈ s → β x`. -/ --- A copy of forall notation from `Std.Util.ExtendedBinder` for pi notation -syntax "Π " binderIdent binderPred ", " term : term - -macro_rules - | `(Π $x:ident $pred:binderPred, $p) => - `(Π $x:ident, satisfies_binder_pred% $x $pred → $p) - | `(Π _ $pred:binderPred, $p) => - `(Π x, satisfies_binder_pred% x $pred → $p) - -/-- Since pi notation and forall notation are interchangable, we can -parse it by simply using the forall parser. -/ -@[macro PiNotation.piNotation] def replacePiNotation : Lean.Macro - | .node info _ args => return .node info ``Lean.Parser.Term.forall args - | _ => Lean.Macro.throwUnsupported /-- Override the Lean 4 pi notation delaborator with one that uses `Π`. Note that this takes advantage of the fact that `(x : α) → p x` notation is never used for propositions, so we can match on this result and rewrite it. -/ @[delab forallE] -def delabPi : Delab := whenPPOption Lean.getPPNotation do +def delabPi' : Delab := whenPPOption Lean.getPPNotation do let stx ← delabForall -- Replacements let stx : Term ← @@ -64,9 +40,6 @@ def delabPi : Delab := whenPPOption Lean.getPPNotation do | `(Π $group, Π $groups*, $body) => `(Π $group $groups*, $body) | _ => pure stx --- the above delaborator and parser are still needed: --- #check Π (x : Nat), Vector Bool x - end PiNotation section SupInfNotation diff --git a/lake-manifest.json b/lake-manifest.json index 98e14120..9634439b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"git": {"url": "https://github.com/leanprover-community/mathlib4", "subDir?": null, - "rev": "8ec1ec7da4a2b6d6865c3b84ea1c6d02b55d97a1", + "rev": "2937b757f71325e24d8b2f6c732cd9a61f590e74", "opts": {}, "name": "mathlib", "inputRev?": "master",