Products of rings and fields

DefinitionCoordinate restriction#✓fully proved

Let \(K\) be a field and \((F_i)_{i \in \iota}\) a family of fields that are \(K\)-algebras indexed by a type \(\iota\). For a finite subset \(S \subseteq \iota\), the coordinate restriction is the \(K\)-algebra homomorphism \(\prod_{i \in \iota} F_i \to \prod_{i \in S} F_i\) sending \((x_i)_{i \in \iota}\) to \((x_i)_{i \in S}\).

public def restrict (S : Finset ι) : (∀ i, F i) →ₐ[K] (∀ i : S, F i) :=
  AlgHom.pi (A := fun i : S => F (i : ι))
    (fun i : S => Pi.evalAlgHom K F (i : ι))

Used by 4

Used bySurjections from a finite product of fields are coordinate restrictions up to isomorphism · Kernel of coordinate restriction · Coordinates of a restriction · Coordinate restriction is surjective

TheoremCoordinates of a restriction#✓fully proved

Let \(K\) be a field, \((F_i)_{i \in \iota}\) a family of fields that are \(K\)-algebras indexed by a type \(\iota\), and \(S \subseteq \iota\) a finite subset. For \(x \in \prod_{i \in \iota} F_i\) and \(s \in S\), the \(s\)-th coordinate of the coordinate restriction of \(x\) to \(S\) is \(x_s\).

@[simp]
public theorem restrict_apply (S : Finset ι) (x : ∀ i, F i) (s : S) :
    restrict (K := K) (F := F) S x s = x s

Uses 1 · Used by 1

Statement usesCoordinate restriction

Used byKernel of coordinate restriction

TheoremCoordinate restriction is surjective#✓fully proved

Let \(K\) be a field, \((F_i)_{i \in \iota}\) a family of fields that are \(K\)-algebras indexed by a type \(\iota\), and \(S \subseteq \iota\) a finite subset. The coordinate restriction \(\prod_{i \in \iota} F_i \to \prod_{i \in S} F_i\) is surjective.

A preimage is obtained by extending by zero outside \(S\).

public theorem restrict_surjective (S : Finset ι) :
    Function.Surjective (restrict (F := F) (K := K) S)

Uses 1 · Used by 1

Statement usesCoordinate restriction

Used bySurjections from a finite product of fields are coordinate restrictions up to isomorphism

TheoremKernel of coordinate restriction#✓fully proved

Let \(K\) be a field, \((F_i)_{i \in \iota}\) a family of fields that are \(K\)-algebras indexed by a type \(\iota\), and \(S \subseteq \iota\) a finite subset. An element \(x \in \prod_{i \in \iota} F_i\) is sent to \(0\) by the coordinate restriction \(\prod_{i \in \iota} F_i \to \prod_{i \in S} F_i\) if and only if \(x_i = 0\) for every \(i \in S\).

public theorem mem_ker_restrict_iff (S : Finset ι) (x : ∀ i, F i) :
    restrict (K := K) (F := F) S x = 0 ↔ ∀ i ∈ S, x i = 0

Uses 2 · Used by 1

Statement usesCoordinate restriction

Proof usesCoordinates of a restriction

Used bySurjections from a finite product of fields are coordinate restrictions up to isomorphism

DefinitionSelected indices of a homomorphism#✓fully proved

Let \(K\) be a field, \(\iota\) a finite type, \((F_i)_{i \in \iota}\) a family of fields that are \(K\)-algebras, \(B\) a commutative \(K\)-algebra and \(\varphi : \prod_{i \in \iota} F_i \to B\) a \(K\)-algebra homomorphism. The selected indices of \(\varphi\) form the finite set of those \(i \in \iota\) for which the ideal of \(F_i\) generated by the image of \(\ker \varphi\) under the \(i\)-th projection \(\prod_{j \in \iota} F_j \to F_i\) is zero.

public noncomputable def selected (φ : (∀ i, F i) →ₐ[K] B) : Finset ι := by
  classical
  haveI := Fintype.ofFinite ι
  exact Finset.univ.filter
    fun i => Ideal.map (Pi.evalRingHom _ i) (RingHom.ker φ) = ⊥

Used by 2

Used bySurjections from a finite product of fields are coordinate restrictions up to isomorphism · Membership in the selected indices

TheoremMembership in the selected indices#✓fully proved

Let \(K\) be a field, \(\iota\) a finite type, \((F_i)_{i \in \iota}\) a family of fields that are \(K\)-algebras, \(B\) a commutative \(K\)-algebra and \(\varphi : \prod_{i \in \iota} F_i \to B\) a \(K\)-algebra homomorphism. An index \(i \in \iota\) belongs to the selected indices of \(\varphi\) if and only if the ideal of \(F_i\) generated by the image of \(\ker \varphi\) under the \(i\)-th projection \(\prod_{j \in \iota} F_j \to F_i\) is zero.

public theorem mem_selected (φ : (∀ i, F i) →ₐ[K] B) (i : ι) :
    i ∈ selected φ ↔
      Ideal.map (Pi.evalRingHom _ i) (RingHom.ker φ) = ⊥

Uses 1 · Used by 1

Statement usesSelected indices of a homomorphism

Used bySurjections from a finite product of fields are coordinate restrictions up to isomorphism

TheoremKernel membership in a finite product of fields is componentwise#✓fully proved

Let \(K\) be a field, \(\iota\) a finite type, \((F_i)_{i \in \iota}\) a family of fields that are \(K\)-algebras, \(B\) a commutative \(K\)-algebra and \(\varphi : \prod_{i \in \iota} F_i \to B\) a \(K\)-algebra homomorphism. For \(x \in \prod_{i \in \iota} F_i\), \(\varphi(x) = 0\) if and only if for every \(i \in \iota\) the coordinate \(x_i\) lies in the ideal of \(F_i\) generated by the image of \(\ker \varphi\) under the \(i\)-th projection \(\prod_{j \in \iota} F_j \to F_i\).

public theorem mem_ker_iff (φ : (∀ i, F i) →ₐ[K] B) (x : ∀ i, F i) :
    φ x = 0 ↔ ∀ i, x i ∈ Ideal.map (Pi.evalRingHom _ i) (RingHom.ker φ)

Used by 1

Used bySurjections from a finite product of fields are coordinate restrictions up to isomorphism

TheoremSurjections from a finite product of fields are coordinate restrictions up to isomorphism#✓fully proved

Let \(K\) be a field, \(\iota\) a finite type, \((F_i)_{i \in \iota}\) a family of fields that are \(K\)-algebras, and \(B\) a commutative \(K\)-algebra. For every surjective \(K\)-algebra homomorphism \(\varphi : \prod_{i \in \iota} F_i \to B\) there are a finite subset \(S \subseteq \iota\) and a \(K\)-algebra isomorphism \(e : B \to \prod_{i \in S} F_i\) such that \(e \circ \varphi\) is the coordinate restriction \((x_i)_{i \in \iota} \mapsto (x_i)_{i \in S}\).

public theorem exists_algEquiv_restrict
    (φ : (∀ i, F i) →ₐ[K] B) (hφ : Function.Surjective φ) :
    ∃ S : Finset ι, ∃ e : B ≃ₐ[K] (∀ i : S, F i),
      e.toAlgHom.comp φ = AlgHom.pi (fun i : S => Pi.evalAlgHom K F i)

Uses 6 · Used by 2

Proof usesKernel membership in a finite product of fields is componentwise · Kernel of coordinate restriction · Membership in the selected indices · Coordinate restriction · Coordinate restriction is surjective · Selected indices of a homomorphism

Used byA surjective image of a finite product of fields is isomorphic to a subproduct · Uniqueness of a finite product of fields up to permutation

TheoremA surjective image of a finite product of fields is isomorphic to a subproduct#✓fully proved

Let \(K\) be a field, \(\iota\) a finite type, \((F_i)_{i \in \iota}\) a family of fields that are \(K\)-algebras, and \(B\) a commutative \(K\)-algebra. If \(\varphi : \prod_{i \in \iota} F_i \to B\) is a surjective \(K\)-algebra homomorphism, then there is a finite subset \(S \subseteq \iota\) such that \(B\) is isomorphic as a \(K\)-algebra to \(\prod_{i \in S} F_i\).

public theorem exists_algEquiv
    (φ : (∀ i, F i) →ₐ[K] B) (hφ : Function.Surjective φ) :
    ∃ S : Finset ι, Nonempty (B ≃ₐ[K] (∀ i : S, F i))

Uses 1

Proof usesSurjections from a finite product of fields are coordinate restrictions up to isomorphism

TheoremUniqueness of a finite product of fields up to permutation#✓fully proved

Let \(K\) be a field, and let \((F_i)_{i \in I}\) and \((G_j)_{j \in J}\) be families of fields that are \(K\)-algebras, indexed by finite types \(I\) and \(J\). If \(e : \prod_{i \in I} F_i \to \prod_{j \in J} G_j\) is an isomorphism of \(K\)-algebras, then there is a bijection \(\sigma : I \to J\) such that \(F_i\) is isomorphic to \(G_{\sigma(i)}\) as a \(K\)-algebra for every \(i \in I\).

public theorem exists_indexEquiv_algEquiv
    {K : Type u} [Field K]
    {ι : Type v} [Finite ι] {κ : Type w} [Finite κ]
    {F : ι → Type x} [∀ i, Field (F i)] [∀ i, Algebra K (F i)]
    {G : κ → Type y} [∀ j, Field (G j)] [∀ j, Algebra K (G j)]
    (e : (∀ i, F i) ≃ₐ[K] (∀ j, G j)) :
    ∃ σ : ι ≃ κ, ∀ i, Nonempty (F i ≃ₐ[K] G (σ i))

Sources

• ATLAS N83, Corollary 4.33.

Uses 1

Proof usesSurjections from a finite product of fields are coordinate restrictions up to isomorphism

TheoremProduct decompositions and idempotents#✓fully proved

A commutative ring \(Q\) is isomorphic to a product \(R \times S\) of two nontrivial rings \(R\) and \(S\) if and only if \(Q\) contains an idempotent \(e\) with \(e \neq 0\) and \(e \neq 1\).

In the reverse direction the two factors are the quotients \(Q/(e)\) and \(Q/(1 - e)\).

theorem ring_product_iff_nontrivial_idempotent (Q : Type u) [CommRing Q] :
    (∃ (R S : Type u) (_ : Ring R) (_ : Ring S) (_ : Nontrivial R) (_ : Nontrivial S),
      Nonempty (Q ≃+* R × S)) ↔
    (∃ e : Q, IsIdempotentElem e ∧ e ≠ 0 ∧ e ≠ 1)

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.