Algebra homomorphisms into an algebraically closed field

TheoremGeometric points detect elements when the generic fiber is reduced#✓fully proved

An element of a torsion-free algebra that vanishes under every algebra homomorphism into an algebraically closed field is zero, provided the tensor product with the fraction field is reduced and finite.

This is the Nullstellensatz-style statement that points detect functions: it is used to show maps of schemes are determined by their values on geometric points, to pass from vanishing on fibers to vanishing globally, and to prove reducedness from pointwise vanishing.

theorem eq_zero_of_forall_algHom_apply_eq_zero_of_isReduced_tensorProduct
    {R : Type u} [CommRing R] [IsDomain R] (K : Type u) [Field K] [Algebra R K]
    [IsFractionRing R K] {B : Type u} [CommRing B] [Algebra R B]
    [NoZeroSMulDivisors R B] [IsReduced (TensorProduct R K B)]
    [Module.Finite K (TensorProduct R K B)] (Ω : Type u) [Field Ω] [IsAlgClosed Ω]
    [Algebra R Ω] [Algebra K Ω] [IsScalarTower R K Ω] (b : B)
    (hb : ∀ φ : B →ₐ[R] Ω, φ b = 0) : b = 0

TheoremCounting algebra homomorphisms from an étale algebra#✓fully proved

Over an algebraically closed field, the number of algebra homomorphisms from an étale algebra to the base field equals its rank.

theorem Algebra.Etale.natCard_algHom_eq_finrank_of_isAlgClosed
    (k : Type*) [Field k] [IsAlgClosed k] (R : Type*) [CommRing R] [Algebra k R]
    [Algebra.Etale k R] :
    Nat.card (R →ₐ[k] k) = Module.finrank k R

Used by 1

Used byCounting algebra homomorphisms of a finite reduced algebra

TheoremCounting algebra homomorphisms of a finite reduced algebra#✓fully proved

A finite reduced algebra over an algebraically closed field has finrank many algebra homomorphisms to the field.

theorem AlgHom.natCard_eq_finrank_of_isReduced_of_isAlgClosed
    (K B : Type*) [Field K] [IsAlgClosed K] [CommRing B] [Algebra K B]
    [Module.Finite K B] [IsReduced B] :
    Nat.card (B →ₐ[K] K) = Module.finrank K B

Uses 1

Proof usesCounting algebra homomorphisms from an étale algebra

TheoremA tensor vanishing at all pairs of algebraic points is zero#✓fully proved

If the scalar-extended evaluation map is injective, a tensor vanishing at all pairs of selected algebraic points is zero. The algebra and the point index may be infinite; no closedness or perfection assumption is needed.

theorem eq_zero_of_forall_lift_apply_eq_zero
    (hinj : Function.Injective
      (lift (Algebra.ofId L (P → L)) (AlgHom.pi pt)
        (fun _ _ => Commute.all _ _) : L ⊗[K] A →ₐ[L] (P → L)))
    (x : A ⊗[K] A)
    (hx : ∀ p q, lift (pt p) (pt q) (fun _ _ => Commute.all _ _) x = 0) : x = 0

TheoremAlgebra maps from relation-preserving generator assignments#✓fully proved

A unital, multiplicatively consistent assignment on generators extends to an algebra homomorphism when it preserves every finite linear relation.

The index family need not be injective or finite; the target may have zero divisors. This preserves the full statement of the source theorem exists_algHom_adjoin_range_apply_eq_of_forall_sum_smul_eq_zero_of_algebra.

theorem exists_algHom_adjoin_of_linearRelations
    {K : Type*} [Field K] {F : Type*} [CommRing F] [Algebra K F]
    (L : Type*) [CommRing L] [Algebra K L]
    {ι : Type*} (t : ι → F) (a : ι → L)
    (hone : ∃ i₀, t i₀ = 1 ∧ a i₀ = 1)
    (hmul : ∀ i j, ∃ k, t k = t i * t j ∧ a k = a i * a j)
    (hcons : ∀ (n : ℕ) (idx : Fin n → ι) (c : Fin n → K),
      ∑ l, c l • t (idx l) = 0 → ∑ l, c l • a (idx l) = 0) :
    ∃ χ : adjoin K (Set.range t) →ₐ[K] L,
      ∀ i, χ ⟨t i, subset_adjoin (Set.mem_range_self i)⟩ = a i

TheoremExtending a ring character via prime-subfield-valued linear forms#✓fully proved

A ring character extends to the algebra generated by another ring image when its kernel contains the first kernel and a separating family of linear forms takes prime-subfield values on that image.

The ambient algebra may be noncommutative, and the separating family may be infinite. The prime subfield is ⊥ : Subfield κ, in any characteristic. This is the source theorem exists_algHom_adjoin_range_apply_eq_of_forall_apply_mem_bot.

theorem exists_algHom_adjoin_of_primeSubfield
    {κ : Type*} [Field κ] {B : Type*} [Ring B] [Algebra κ B]
    {ι : Type*} (c : ι → (B →ₗ[κ] κ)) (hc : ∀ b : B, (∀ i, c i b = 0) → b = 0)
    {T : Type*} [CommRing T] (red : T →+* B) (ρ : T →+* κ)
    (hbot : ∀ (t : T) (i : ι), c i (red t) ∈ (⊥ : Subfield κ))
    (hker : ∀ t : T, red t = 0 → ρ t = 0) :
    ∃ χ : adjoin κ (Set.range red) →ₐ[κ] κ,
      ∀ t : T, χ ⟨red t, subset_adjoin (Set.mem_range_self t)⟩ = ρ t

TheoremLifting maps to algebraically closed fields along integral extensions#✓fully proved

A homomorphism from R to an algebraically closed field extends to an integral extension S with any prescribed prime kernel lying over ker χ.

This is the key step for extending points of a scheme along integral morphisms, for going-up arguments, and for lifting maps through integral closures: the kernel control RingHom.ker χ' = Q says the lifted map has exactly the prescribed residue behavior.

theorem exists_comp_algebraMap_eq_and_ker_eq_of_isIntegral_of_isAlgClosed
    {R S K : Type*} [CommRing R] [CommRing S] [Algebra R S] [Algebra.IsIntegral R S]
    [Field K] [IsAlgClosed K] (χ : R →+* K)
    (Q : Ideal S) [Q.IsPrime] (hQ : Q.comap (algebraMap R S) = RingHom.ker χ) :
    ∃ χ' : S →+* K, χ'.comp (algebraMap R S) = χ ∧ RingHom.ker χ' = Q

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.