General topics, history and foundations

TheoremAx–Grothendieck theorem#

The Ax-Grothendieck theorem

If K is an algebraically closed field, and S : Set (ι → K) is the zeroLocus of an ideal of the multivariable polynomial ring, then any injective polynomial map S → S is also surjective on S.

ax_grothendieck_zeroLocus.{u_1, u_2} {K : Type u_1} {ι : Type u_2} [Field K] [IsAlgClosed K]
  [Finite ι] (I : Ideal (MvPolynomial ι K)) (p : ι → MvPolynomial ι K) :
  have S := MvPolynomial.zeroLocus K I;
  Set.MapsTo (fun v i => (MvPolynomial.eval v) (p i)) S S →
    Set.InjOn (fun v i => (MvPolynomial.eval v) (p i)) S →
      Set.SurjOn (fun v i => (MvPolynomial.eval v) (p i)) S S
Sources
Mathlibax_grothendieck_zeroLocus
Uses 13
Statement usesAlgebraically closed field · Associative algebra over a commutative ring · Ideal of a commutative ring · Polynomial in several indeterminates
Proof usesCharacteristic of a ring · Characteristic p · Definable set · Existence of algebraic closure of a field · Local ring · Noetherian module · Noetherian ring · Satisfiability · Sum of subspaces

TheoremBoolean prime ideal theorem#

Mathlib states this as DistribLattice.prime_ideal_of_disjoint_filter_ideal.

DistribLattice.prime_ideal_of_disjoint_filter_ideal.{u_1} {α : Type u_1} [DistribLattice α]
  {F : Order.PFilter α} {I : Order.Ideal α} (hFI : Disjoint ↑F ↑I) :
  ∃ J, J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J

This is the prime ideal separation theorem for (bounded) distributive lattices, of which the Boolean prime ideal theorem is a special case.

Sources
MathlibDistribLattice.prime_ideal_of_disjoint_filter_ideal
Uses 1
Statement usesSet

TheoremKleene's recursion theorem#

Kleene's second recursion theorem

Nat.Partrec.Code.fixed_point₂ {f : Nat.Partrec.Code → ℕ →. ℕ} (hf : Partrec₂ f) : ∃ c, c.eval = f c
Sources
MathlibNat.Partrec.Code.fixed_point₂
Uses 5 · Used by 1
Statement usesNatural number
Proof usesIn terms of general recursive functions · Integer · List · Primitive recursive function
Used byRice theorem

TheoremKönig's theorem (set theory)#

König's theorem

Cardinal.sum_lt_prod.{u_1, u_2} {ι : Type u_1} (f g : ι → Cardinal.{u_2})
  (H : ∀ (i : ι), f i < g i) : Cardinal.sum f < Cardinal.prod g
Sources
MathlibCardinal.sum_lt_prod
Uses 2
Statement usesCardinal
Proof usesNatural number

TheoremSzpilrajn extension theorem#

Szpilrajn extension theorem: any partial order can be extended to a linear order.

extend_partialOrder.{u} {α : Type u} (r : α → α → Prop) [IsPartialOrder α r] :
  ∃ s, IsLinearOrder α s ∧ r ≤ s
Sources
Mathlibextend_partialOrder
Uses 1
Proof usesSet

TheoremWell-ordering theorem#

The well-ordering theorem (or Zermelo's theorem): every type can be well-ordered.

exists_wellFoundedLT.{u} (α : Type u) : ∃ x, WellFoundedLT α
Sources
Mathlibexists_wellFoundedLT
Uses 1
Proof usesCardinal

TheoremŁoś' theorem#

Łoś's Theorem: A sentence is true in an ultraproduct if and only if the set of structures it is true in is in the ultrafilter.

FirstOrder.Language.Ultraproduct.sentence_realize.{u, v, u_1, u_2} {α : Type u_1} {M : α → Type u_2}
  {u : Ultrafilter α} {L : FirstOrder.Language} [(a : α) → L.Structure (M a)]
  [∀ (a : α), Nonempty (M a)] (φ : L.Sentence) : (↑u).Product M ⊨ φ ↔ ∀ᶠ (a : α) in ↑u, M a ⊨ φ
Sources
MathlibFirstOrder.Language.Ultraproduct.sentence_realize
Uses 3 · Used by 1
Statement usesFilter · First-order formula · First-order structure
Used byCompactness theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.