Documentation

GeometricallyP.Algebra.GeometricallyIrreducible

Geometrically irreducible algebras #

In this file we develop the theory of geometrically irreducible algebras over a field.

References #

source
class Algebra.GeometricallyIrreducible (k : Type u_2) (R : Type u_3) [Field k] [CommRing R] [Algebra k R] :
Prop

A k-algebra R is geometrically irreducible if Spec (AlgebraicClosure k ⊗[k] R) is irreducible. In this case, Spec (K ⊗[k] R) is irreducible for every field extension K of k (see Algebra.GeometricallyIrreducible.irreducibleSpace). Note: The stacks project definition is the latter condition, which is equivalent to the former by the above. The reason for choosing this definition is that it does not quantify over types.

Instances
    source
    theorem Algebra.geometricallyIrreducible_iff (k : Type u_2) (R : Type u_3) [Field k] [CommRing R] [Algebra k R] :
    GeometricallyIrreducible k R ↔ IrreducibleSpace (PrimeSpectrum (TensorProduct k (AlgebraicClosure k) R))
    source
    theorem Algebra.GeometricallyIrreducible.iff_irreducibleSpace_separableClosure (k : Type u) (R : Type u_2) [CommRing R] [Field k] [Algebra k R] :
    GeometricallyIrreducible k R ↔ IrreducibleSpace (PrimeSpectrum (TensorProduct k (SeparableClosure k) R))

    Stacks Tag 037K ((3) <=> (4))

    source
    theorem Algebra.GeometricallyIrreducible.of_forall_irreducibleSpace_of_isSeparable (k : Type u) (R : Type u_2) [CommRing R] [Field k] [Algebra k R] (H : ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra k K] [Module.Finite k K] [Algebra.IsSeparable k K], IrreducibleSpace (PrimeSpectrum (TensorProduct k K R))) :
    GeometricallyIrreducible k R

    If Spec (K ⊗[k] R) is irreducible for every finite separable extension K of k, then R is geometrically irreducible over k.

    source
    theorem Algebra.GeometricallyIrreducible.irreducibleSpace (k : Type u) (R : Type u_2) [CommRing R] [Field k] [Algebra k R] [GeometricallyIrreducible k R] (K : Type u_3) [Field K] [Algebra k K] :
    IrreducibleSpace (PrimeSpectrum (TensorProduct k K R))

    If R is geometrically irreducible over k, for every field extension K of k, the prime spectrum Spec (K ⊗[k] R) is irreducible.

    source
    theorem Algebra.GeometricallyIrreducible.irreducibleSpace' (k : Type u) (R : Type u_2) [CommRing R] [Field k] [Algebra k R] [GeometricallyIrreducible k R] (K : Type u_3) [Field K] [Algebra k K] :
    IrreducibleSpace (PrimeSpectrum (TensorProduct k R K))

    If R is geometrically irreducible over k, for every field extension K of k, the prime spectrum Spec (K ⊗[k] R) is irreducible.

    source
    theorem Algebra.GeometricallyIrreducible.of_irreducibleSpace_of_isSepClosed (k : Type u) (R : Type u_2) [CommRing R] [Field k] [Algebra k R] (Ω : Type u_3) [Field Ω] [Algebra k Ω] [IsSepClosed Ω] (H : IrreducibleSpace (PrimeSpectrum (TensorProduct k Ω R))) :
    GeometricallyIrreducible k R

    If Ω is a separably closed extension of k such that Spec (Ω ⊗[k] R) is irreducible, R is geometrically irreducible over k.

    source
    theorem Algebra.GeometricallyIrreducible.isField_tensorProduct_of_isSeparable (k : Type u_3) (K : Type u_4) (L : Type u_5) [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] [Module.Finite k K] [Algebra.IsSeparable k K] [GeometricallyIrreducible k L] :
    IsField (TensorProduct k L K)

    If K/k is a finte separable extension and L a geometrically irreducible field over k then L ⊗[k] K is a field

    source
    theorem Algebra.GeometricallyIrreducible.trans (k : Type u) (R : Type u_2) [CommRing R] [Field k] [Algebra k R] (K : Type u_3) [Field K] [Algebra k K] [Algebra K R] [IsScalarTower k K R] [GeometricallyIrreducible k K] [GeometricallyIrreducible K R] :
    GeometricallyIrreducible k R

    If K is geometrically irreducible over k and R is geometrically irreducible over K, then R is geometrically irreducible over k.

    source
    theorem Algebra.GeometricallyIrreducible.iff_of_forall_isSeparable_mem (k : Type u) [Field k] (K : Type u_3) [Field K] [Algebra k K] :
    GeometricallyIrreducible k K ↔ ∀ (x : K), IsSeparable k x → x ∈ Set.range ⇑(algebraMap k K)

    Let K over kbe a field extension. ThenKis geometrically irreducible overkif and only if everyk-separable, algebraic element x : Kis contained ink`.