Add 09GY lemma to AlgebraicClosure.lean

.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)
@@ -195,17 +176,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: |

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]

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

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
@@ -413,4 +416,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

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

@@ -74,6 +74,10 @@ 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 :=
   exists_root_of_splits _ (IsAlgClosed.splits p) hp
 
@@ -119,6 +123,11 @@ 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
 
+
+/--
+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) :
     IsAlgClosed k := by
   refine ⟨fun p ↦ Or.inr ?_⟩
@@ -145,6 +154,10 @@ theorem of_ringEquiv (k' : Type u) [Field k'] (e : k ≃+* k')
   clear hx hpe hp hmp
   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) :
     p.degree = 1 :=
   degree_eq_one_of_irreducible_of_splits hp (IsAlgClosed.splits_codomain _)
@@ -181,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: 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] :
     L = ⊥ := bot_unique fun x hx ↦ by
@@ -199,7 +215,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
@@ -262,7 +280,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
@@ -308,7 +329,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