From 2a71c88a439a60b189bf0a8dd06ad9f9dff0ae70 Mon Sep 17 00:00:00 2001 From: jjdishere Date: Sat, 24 Aug 2024 01:01:45 +0200 Subject: [PATCH 01/10] first tag --- Mathlib/Algebra/Field/Defs.lean | 4 +++- Mathlib/Algebra/Field/Subfield.lean | 4 +++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Field/Defs.lean b/Mathlib/Algebra/Field/Defs.lean index 4943b798adf4c9..1231c183313ff9 100644 --- a/Mathlib/Algebra/Field/Defs.lean +++ b/Mathlib/Algebra/Field/Defs.lean @@ -171,7 +171,9 @@ to control the specific definitions for some special cases of `K` (in particular See also note [forgetful inheritance]. If the field has positive characteristic `p`, our division by zero convention forces -`ratCast (1 / p) = 1 / 0 = 0`. -/ +`ratCast (1 / p) = 1 / 0 = 0`. + +[Stacks: Definition 09FD, first part](https://stacks.math.columbia.edu/tag/09FD) -/ class Field (K : Type u) extends CommRing K, DivisionRing K -- see Note [lower instance priority] diff --git a/Mathlib/Algebra/Field/Subfield.lean b/Mathlib/Algebra/Field/Subfield.lean index b304f131e2f96e..ac7d7e79eaa40b 100644 --- a/Mathlib/Algebra/Field/Subfield.lean +++ b/Mathlib/Algebra/Field/Subfield.lean @@ -145,7 +145,9 @@ end SubfieldClass /-- `Subfield R` is the type of subfields of `R`. A subfield of `R` is a subset `s` that is a multiplicative submonoid and an additive subgroup. Note in particular that it shares the - same 0 and 1 as R. -/ + same 0 and 1 as R. + + [Stacks: Definition 09FD, second part](https://stacks.math.columbia.edu/tag/09FD) -/ structure Subfield (K : Type u) [DivisionRing K] extends Subring K where /-- A subfield is closed under multiplicative inverses. -/ inv_mem' : ∀ x ∈ carrier, x⁻¹ ∈ carrier From a99968cfddc3c12fb655c6730d170b757d8ab944 Mon Sep 17 00:00:00 2001 From: zjj Date: Tue, 27 Aug 2024 04:25:42 +0100 Subject: [PATCH 02/10] 09GR + 09GS + 09GT --- .../FieldTheory/IsAlgClosed/AlgebraicClosure.lean | 5 ++++- Mathlib/FieldTheory/IsAlgClosed/Basic.lean | 14 +++++++++++++- 2 files changed, 17 insertions(+), 2 deletions(-) diff --git a/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean b/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean index bef0b0e2de8f44..8e4d4e13142daf 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean @@ -346,7 +346,10 @@ attribute [local instance] AlgebraicClosureAux.field AlgebraicClosureAux.instAlg AlgebraicClosureAux.instIsAlgClosed /-- The canonical algebraic closure of a field, the direct limit of adding roots to the field for -each polynomial over the field. -/ +each polynomial over the field. + +[Stacks: Lemma 09GT](https://stacks.math.columbia.edu/tag/09GT) +-/ def AlgebraicClosure : Type u := MvPolynomial (AlgebraicClosureAux k) k ⧸ RingHom.ker (MvPolynomial.aeval (R := k) id).toRingHom diff --git a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean index f50d91d7f2c113..639fb34c2a5ac3 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean @@ -74,6 +74,9 @@ namespace IsAlgClosed variable {k} +/-- +* [Stacks: Lemma 09GR, (4) ⟹ (3)](https://stacks.math.columbia.edu/tag/09GR) +-/ theorem exists_root [IsAlgClosed k] (p : k[X]) (hp : p.degree ≠ 0) : ∃ x, IsRoot p x := exists_root_of_splits _ (IsAlgClosed.splits p) hp @@ -119,6 +122,10 @@ theorem exists_aeval_eq_zero {R : Type*} [Field R] [IsAlgClosed k] [Algebra R k] (hp : p.degree ≠ 0) : ∃ x : k, aeval x p = 0 := exists_eval₂_eq_zero (algebraMap R k) p hp + +/-- +* [Stacks: Lemma 09GR, (3) ⟹ (4)](https://stacks.math.columbia.edu/tag/09GR) +-/ theorem of_exists_root (H : ∀ p : k[X], p.Monic → Irreducible p → ∃ x, p.eval x = 0) : IsAlgClosed k := by refine ⟨fun p ↦ Or.inr ?_⟩ @@ -145,6 +152,9 @@ theorem of_ringEquiv (k' : Type u) [Field k'] (e : k ≃+* k') clear hx hpe hp hmp induction p using Polynomial.induction_on <;> simp_all +/-- +* [Stacks: Lemma 09GR, (4) ⟹ (2)](https://stacks.math.columbia.edu/tag/09GR) +-/ theorem degree_eq_one_of_irreducible [IsAlgClosed k] {p : k[X]} (hp : Irreducible p) : p.degree = 1 := degree_eq_one_of_irreducible_of_splits hp (IsAlgClosed.splits_codomain _) @@ -199,7 +209,9 @@ lemma Polynomial.isCoprime_iff_aeval_ne_zero_of_isAlgClosed (K : Type v) [Field simpa only [degree_map] using (ne_of_lt <| degree_pos_of_ne_zero_of_nonunit h0 hu).symm exact not_and_or.mpr (h a) (by simp_rw [map_mul, ← eval_map_algebraMap, ha, zero_mul, true_and]) -/-- Typeclass for an extension being an algebraic closure. -/ +/-- Typeclass for an extension being an algebraic closure. +[Stacks: Definition 09GS](https://stacks.math.columbia.edu/tag/09GS) + -/ class IsAlgClosure (R : Type u) (K : Type v) [CommRing R] [Field K] [Algebra R K] [NoZeroSMulDivisors R K] : Prop where alg_closed : IsAlgClosed K From 2b9d2b98a867e86a1ee7d0c25cc3c58e9a5fc81f Mon Sep 17 00:00:00 2001 From: zjj Date: Tue, 27 Aug 2024 04:29:48 +0100 Subject: [PATCH 03/10] comment --- Mathlib/FieldTheory/IsAlgClosed/Basic.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean index 639fb34c2a5ac3..fd0291441f6684 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean @@ -75,6 +75,7 @@ namespace IsAlgClosed variable {k} /-- +If `k` is algebraically closed, then every nonconstant polynomial has a root. * [Stacks: Lemma 09GR, (4) ⟹ (3)](https://stacks.math.columbia.edu/tag/09GR) -/ theorem exists_root [IsAlgClosed k] (p : k[X]) (hp : p.degree ≠ 0) : ∃ x, IsRoot p x := @@ -124,6 +125,7 @@ theorem exists_aeval_eq_zero {R : Type*} [Field R] [IsAlgClosed k] [Algebra R k] /-- +If every nonconstant polynomial over `k` has a root, then `k` is algebraically closed. * [Stacks: Lemma 09GR, (3) ⟹ (4)](https://stacks.math.columbia.edu/tag/09GR) -/ theorem of_exists_root (H : ∀ p : k[X], p.Monic → Irreducible p → ∃ x, p.eval x = 0) : @@ -153,6 +155,7 @@ theorem of_ringEquiv (k' : Type u) [Field k'] (e : k ≃+* k') induction p using Polynomial.induction_on <;> simp_all /-- +If `k` is algebraically closed, then every irreducible polynomial over `k` is linear. * [Stacks: Lemma 09GR, (4) ⟹ (2)](https://stacks.math.columbia.edu/tag/09GR) -/ theorem degree_eq_one_of_irreducible [IsAlgClosed k] {p : k[X]} (hp : Irreducible p) : From 42b281d78cb8589d4cfba6cab8da28892ac08f09 Mon Sep 17 00:00:00 2001 From: zjj Date: Tue, 27 Aug 2024 04:33:53 +0100 Subject: [PATCH 04/10] finish 10 --- Mathlib/FieldTheory/IsAlgClosed/Basic.lean | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean index fd0291441f6684..fd15352771c316 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean @@ -277,7 +277,10 @@ private instance FractionRing.isAlgebraic : (Algebra.IsAlgebraic.isAlgebraic _) /-- A (random) homomorphism from an algebraic extension of R into an algebraically - closed extension of R. -/ + closed extension of R. + +[Stacks: Lemma 09GU](https://stacks.math.columbia.edu/tag/09GU) +-/ noncomputable irreducible_def lift : S →ₐ[R] M := by letI : IsDomain R := (NoZeroSMulDivisors.algebraMap_injective R S).isDomain _ letI := FractionRing.liftAlgebra R M @@ -323,7 +326,9 @@ variable (R : Type u) [CommRing R] (L : Type v) (M : Type w) [Field L] [Field M] variable [Algebra R M] [NoZeroSMulDivisors R M] [IsAlgClosure R M] variable [Algebra R L] [NoZeroSMulDivisors R L] [IsAlgClosure R L] -/-- A (random) isomorphism between two algebraic closures of `R`. -/ +/-- A (random) isomorphism between two algebraic closures of `R`. + +* [Stacks: Lemma 09GV](https://stacks.math.columbia.edu/tag/09GV) -/ noncomputable def equiv : L ≃ₐ[R] M := -- Porting note (#10754): added to replace local instance above haveI : IsAlgClosed L := IsAlgClosure.alg_closed R From 3126ac34eb564ed3a3899c1991e0ed9b9ee98183 Mon Sep 17 00:00:00 2001 From: zjj Date: Tue, 27 Aug 2024 04:38:39 +0100 Subject: [PATCH 05/10] delete * --- Mathlib/FieldTheory/IsAlgClosed/Basic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean index fd15352771c316..6f114b59715ec2 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean @@ -76,7 +76,7 @@ variable {k} /-- If `k` is algebraically closed, then every nonconstant polynomial has a root. -* [Stacks: Lemma 09GR, (4) ⟹ (3)](https://stacks.math.columbia.edu/tag/09GR) +[Stacks: Lemma 09GR, (4) ⟹ (3)](https://stacks.math.columbia.edu/tag/09GR) -/ theorem exists_root [IsAlgClosed k] (p : k[X]) (hp : p.degree ≠ 0) : ∃ x, IsRoot p x := exists_root_of_splits _ (IsAlgClosed.splits p) hp @@ -126,7 +126,7 @@ theorem exists_aeval_eq_zero {R : Type*} [Field R] [IsAlgClosed k] [Algebra R k] /-- If every nonconstant polynomial over `k` has a root, then `k` is algebraically closed. -* [Stacks: Lemma 09GR, (3) ⟹ (4)](https://stacks.math.columbia.edu/tag/09GR) +[Stacks: Lemma 09GR, (3) ⟹ (4)](https://stacks.math.columbia.edu/tag/09GR) -/ theorem of_exists_root (H : ∀ p : k[X], p.Monic → Irreducible p → ∃ x, p.eval x = 0) : IsAlgClosed k := by @@ -156,7 +156,7 @@ theorem of_ringEquiv (k' : Type u) [Field k'] (e : k ≃+* k') /-- If `k` is algebraically closed, then every irreducible polynomial over `k` is linear. -* [Stacks: Lemma 09GR, (4) ⟹ (2)](https://stacks.math.columbia.edu/tag/09GR) +[Stacks: Lemma 09GR, (4) ⟹ (2)](https://stacks.math.columbia.edu/tag/09GR) -/ theorem degree_eq_one_of_irreducible [IsAlgClosed k] {p : k[X]} (hp : Irreducible p) : p.degree = 1 := @@ -328,7 +328,7 @@ variable [Algebra R L] [NoZeroSMulDivisors R L] [IsAlgClosure R L] /-- A (random) isomorphism between two algebraic closures of `R`. -* [Stacks: Lemma 09GV](https://stacks.math.columbia.edu/tag/09GV) -/ +[Stacks: Lemma 09GV](https://stacks.math.columbia.edu/tag/09GV) -/ noncomputable def equiv : L ≃ₐ[R] M := -- Porting note (#10754): added to replace local instance above haveI : IsAlgClosed L := IsAlgClosure.alg_closed R From 2ad82c329bd4c886a8d8159c56e69199a34e0fe7 Mon Sep 17 00:00:00 2001 From: zjj Date: Tue, 27 Aug 2024 04:48:04 +0100 Subject: [PATCH 06/10] add 09GR --- Mathlib/FieldTheory/IsAlgClosed/Basic.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean index 6f114b59715ec2..317d1924dbe604 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean @@ -194,7 +194,10 @@ end IsAlgClosed /-- If `k` is algebraically closed, `K / k` is a field extension, `L / k` is an intermediate field which is algebraic, then `L` is equal to `k`. A corollary of -`IsAlgClosed.algebraMap_surjective_of_isAlgebraic`. -/ +`IsAlgClosed.algebraMap_surjective_of_isAlgebraic`. + +[Stacks: Lemma 09GQ, (4) ⟹ (2)](https://stacks.math.columbia.edu/tag/09GQ) +-/ theorem IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic {k K : Type*} [Field k] [Field K] [IsAlgClosed k] [Algebra k K] (L : IntermediateField k K) [Algebra.IsAlgebraic k L] : L = ⊥ := bot_unique fun x hx ↦ by From 173693b6e5c40ffcfe26947f5a16e6d170ef5e43 Mon Sep 17 00:00:00 2001 From: zjj Date: Tue, 27 Aug 2024 04:53:15 +0100 Subject: [PATCH 07/10] refine --- Mathlib/FieldTheory/IsAlgClosed/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean index 317d1924dbe604..fcb94c1ee2630b 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean @@ -196,7 +196,7 @@ end IsAlgClosed which is algebraic, then `L` is equal to `k`. A corollary of `IsAlgClosed.algebraMap_surjective_of_isAlgebraic`. -[Stacks: Lemma 09GQ, (4) ⟹ (2)](https://stacks.math.columbia.edu/tag/09GQ) +[Stacks: Definition 09GQ, Lemma 09GR (4) ⟹ (1)](https://stacks.math.columbia.edu/tag/09GQ) -/ theorem IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic {k K : Type*} [Field k] [Field K] [IsAlgClosed k] [Algebra k K] (L : IntermediateField k K) [Algebra.IsAlgebraic k L] : From ba8b0fd161f769e6022353a0213b28d6abe1f539 Mon Sep 17 00:00:00 2001 From: jjdishere Date: Tue, 27 Aug 2024 14:27:18 +0200 Subject: [PATCH 08/10] CI for fork --- .github/workflows/build_fork.yml | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml index 78c386218fa750..4ae7448de57831 100644 --- a/.github/workflows/build_fork.yml +++ b/.github/workflows/build_fork.yml @@ -195,17 +195,6 @@ jobs: MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }} MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }} - - name: check the cache - run: | - # Because the `lean-pr-testing-NNNN` branches use toolchains that are "updated in place" - # the cache mechanism is unreliable, so we don't test it if we are on such a branch. - if [[ ! $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then - lake exe cache clean! - rm -rf .lake/build/lib/Mathlib - lake exe cache get || (sleep 1; lake exe cache get) - lake build --no-build - fi - - name: build archive id: archive run: | From 41b44b8aa42708ab1894993eb15d40e8a7f94762 Mon Sep 17 00:00:00 2001 From: su00000 Date: Wed, 28 Aug 2024 09:37:42 +0800 Subject: [PATCH 09/10] Update AlgebraicClosure.lean --- .../IsAlgClosed/AlgebraicClosure.lean | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean b/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean index bef0b0e2de8f44..2c9d6ee560bbf1 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean @@ -413,4 +413,25 @@ instance [CharZero k] : CharZero (AlgebraicClosure k) := instance {p : ℕ} [CharP k p] : CharP (AlgebraicClosure k) p := charP_of_injective_algebraMap (RingHom.injective (algebraMap k (AlgebraicClosure k))) p +/-09GY Lemma: Two polynomials in $k[x]$ are relatively prime +precisely when they have no common roots in an algebraic closure $\overline{k}$ of $k$. +[Stacks: Lemma 09GY](https://stacks.math.columbia.edu/tag/09GY) -/ +lemma IsComrime_iff_no_common_root {k : Type*} [Field k] {p q : Polynomial k} : +IsCoprime p q ↔ (¬ ∃ r : AlgebraicClosure k, IsRoot (map (algebraMap k (AlgebraicClosure k)) p) r ∧ +IsRoot (map (algebraMap k (AlgebraicClosure k)) q) r) := by + letI := Classical.typeDecidableEq (AlgebraicClosure k) + rw [← isCoprime_map (algebraMap k (AlgebraicClosure k)), + ← EuclideanDomain.gcd_isUnit_iff, isUnit_iff_degree_eq_zero, iff_not_comm] + constructor + · intro ⟨r, hr⟩ + by_contra h + rw [← isUnit_iff_degree_eq_zero, isUnit_iff] at h + rcases h with ⟨c, unc, polc⟩ + rw [← isRoot_gcd_iff_isRoot_left_right, ← polc, IsRoot.def, eval_C] at hr + rw [hr, isUnit_iff_ne_zero] at unc + exact unc rfl + · intro h + rcases IsAlgClosed.exists_root _ h with ⟨r, hr⟩ + exact ⟨r, isRoot_gcd_iff_isRoot_left_right.mp hr⟩ + end AlgebraicClosure From 082bec088b7098b796b5fcd5d38e18e0d74d2aae Mon Sep 17 00:00:00 2001 From: jjdishere Date: Wed, 28 Aug 2024 14:14:20 +0200 Subject: [PATCH 10/10] remove checkworkflow These is for CI only. revert this when making PR. --- .github/workflows/build_fork.yml | 19 ------------------- 1 file changed, 19 deletions(-) diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml index 4ae7448de57831..541b81944bbfd0 100644 --- a/.github/workflows/build_fork.yml +++ b/.github/workflows/build_fork.yml @@ -86,25 +86,6 @@ jobs: run: | ./scripts/lint-bib.sh - check_workflows: - if: github.repository != 'leanprover-community/mathlib4' - name: check workflows (fork) - runs-on: ubuntu-latest - steps: - - name: cleanup - run: | - find . -name . -o -prune -exec rm -rf -- {} + - - - uses: actions/checkout@v4 - - - name: update workflows - run: | - cd .github/workflows/ - ./mk_build_yml.sh - - - name: check that workflows were consistent - run: git diff --exit-code - build: if: github.repository != 'leanprover-community/mathlib4' name: Build (fork)