TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Hopf quotients, kernels of Hopf maps, and tensor products

Statement

Let $k$ be a field. Let $H$ be a Hopf $k$ -algebra and $I ⊴ H$ a Hopf ideal. The quotient $H / I$ has a unique Hopf structure making the quotient map $q : H \to H / I$ a Hopf map. Every Hopf map $f : H \to K$ that kills $I$ factors uniquely through $q$ as a Hopf map. For any Hopf map $f : H \to K$ , its kernel is a Hopf ideal.

For Hopf $k$ -algebras $H, K$ , the tensor product $H \otimes K$ is a Hopf algebra with multiplication $m_{H \otimes K} = (m_{H} \otimes m_{K}) ({i d}_{H} \otimes τ_{K, H} \otimes {i d}_{K})$ , coproduct $Δ_{H \otimes K} = ({i d}_{H} \otimes τ_{H, K} \otimes {i d}_{K}) (Δ_{H} \otimes Δ_{K})$ , unit $u_{H} \otimes u_{K}$ , counit $ε_{H} \otimes ε_{K}$ , and antipode $S_{H} \otimes S_{K}$ , where $τ$ flips the two middle tensor factors. The quotient and tensor-product constructions are choice-free. AC is assumed for the kernel assertion and is used only for tensor-kernel exactness over arbitrary vector spaces.

Facts & Assumptions

Given: A field $k$ ; Hopf $k$ -algebras $H, K$ ; a Hopf ideal $I ⊴ H$ ; and Hopf maps $f : H \to K$ .

Here a Hopf map means a bialgebra map between Hopf algebras; step 1.4 proves that every such map automatically commutes with antipodes. Sweedler notation $Δ (h) = \sum h_{1} \otimes h_{2}$ denotes a finite tensor expression and is used only inside well-defined linear contractions (Counit uniqueness and finite Sweedler calculus).

[A1]

The Axiom of Choice: every family of nonempty sets has a choice function. It is used only through the arbitrary-vector-space complement step in the tensor-kernel lemma below.

[F1]

Hopf ideals and Hopf subalgebras: a Hopf ideal is a two-sided ideal with $ε (I) = 0$ , $S (I) \subseteq I$ , and $Δ (I)$ in the sum of the images of $I \otimes H$ and $H \otimes I$ ; under AC this is the usual tensor-sum shorthand.

[F2]

A ring homomorphism whose kernel contains a two-sided ideal factors uniquely through the quotient ring: an algebra map that kills a two-sided ideal factors uniquely through the quotient algebra.

[F3]

The tensor product of $R$ -algebras has multiplication $(a \otimes b) (a^{'} \otimes b^{'}) = a a^{'} \otimes b b^{'}$ : multiplication on $A \otimes_{R} B$ is $(a \otimes b) (a^{'} \otimes b^{'}) = a a^{'} \otimes b b^{'}$ , with unit $1_{A} \otimes 1_{B}$ .

[F4]

Bialgebras and bialgebra maps: bialgebra maps preserve multiplication, unit, comultiplication, and counit; $Δ$ and $ε$ are unital algebra maps.

[F5]

Convolution of linear maps is associative and unital: convolution on linear maps is associative and has unit $u_{A} ε_{C}$ .

[F6]

Uniqueness and anti-multiplicativity and anti-comultiplicativity of the antipode: two-sided convolution inverses are unique; antipodes are anti-multiplicative and anti-comultiplicative.

[F7]

Tensoring injections and the kernel of a tensor product of quotient maps over a field: under AC, tensoring injections of vector spaces preserves injectivity, and for quotient maps $p : V \to V / U$ , $q : W \to W / Z$ , $\ker (p \otimes q) = U \otimes W + V \otimes Z$ .

[F8]

Scalars, tensor powers, the empty tensor, opposite algebras and finite sums and Associator naturality, pentagon, unit triangle and symmetry hexagons on elementary tensors: tensor products are over $k$ , every tensor is a finite sum of elementary tensors, and the canonical reassociation and flip maps act on those tensors by reassociation and exchange.

[F9]

Hopf algebras and antipodes: a Hopf algebra has an antipode $S$ satisfying $m (S \otimes i d) Δ = u ε = m (i d \otimes S) Δ$ ; bijectivity of $S$ is not part of the definition.

[F10]

Counit uniqueness and finite Sweedler calculus: Sweedler notation denotes a finite tensor sum, and each contraction is a well-defined linear map on that tensor.

Proof

technique · direct

1.1givenF1F2algebra

The quotient multiplication $(h + I) (h^{'} + I) = h h^{'} + I$ and unit $1_{H} + I$ are well-defined because $I$ is a two-sided ideal; [F2] gives the unique algebra map $q_{I} : H \to H / I$ .

1.2givenF1F8construct

Define $\overline{Δ} (h + I) : = (q_{I} \otimes q_{I}) Δ_{H} (h)$ . If $h - h^{'} \in I$ , then $Δ (h - h^{'})$ lies in the sum of the two tensor images in [F1], and $q_{I} \otimes q_{I}$ kills both, so the formula is independent of the representative. Define $\overline{ε} (h + I) : = ε_{H} (h)$ , which is well-defined by [F1]. These formulas construct linear maps on the quotient directly.

1.3givenF1construct

Define $\overline{S} (h + I) : = S_{H} (h) + I$ . It is well-defined because $S_{H} (I) \subseteq I$ by [F1].

1.4givenF4F5F6F9F10algebra

For any bialgebra map $f : H \to K$ , the maps $S_{K} f$ and $f S_{H}$ are both two-sided convolution inverses of $f$ . Indeed, $(S_{K} f) * f = m_{K} (S_{K} \otimes i d) Δ_{K} f = u_{K} ε_{H}$ and $f * (S_{K} f) = m_{K} (i d \otimes S_{K}) Δ_{K} f = u_{K} ε_{H}$ , using that $f$ is a coalgebra map and both antipode identities in $K$ ; also $(f S_{H}) * f = f m_{H} (S_{H} \otimes i d) Δ_{H} = u_{K} ε_{H}$ and $f * (f S_{H}) = f m_{H} (i d \otimes S_{H}) Δ_{H} = u_{K} ε_{H}$ , using multiplicativity of $f$ and both antipode identities in $H$ . By uniqueness of two-sided inverses in the associative convolution algebra [F5, F6], $S_{K} f = f S_{H}$ .

1.5givenF4algebra

For a Hopf map $f : H \to K$ , $J : = \ker f$ is a two-sided ideal and $ε_{H} (J) = 0$ , since $f$ preserves multiplication, unit, and counit by [F4].

1.6givenA1F2F4F7F10algebra

By [F2], $f = \tilde{f} q_{J}$ for a linear map $\tilde{f} : H / J \to K$ , and $\tilde{f}$ is injective because $\tilde{f} (h + J) = f (h) = 0$ implies $h \in J$ . By [F7], $\tilde{f} \otimes \tilde{f}$ is injective and $\ker (q_{J} \otimes q_{J}) = J \otimes H + H \otimes J$ ; hence $\ker (f \otimes f) = J \otimes H + H \otimes J$ . For $j \in J$ , $(f \otimes f) Δ_{H} (j) = Δ_{K} (f (j)) = 0$ by [F4], so $Δ_{H} (j) \in J \otimes H + H \otimes J$ .

1.7givenF3F8F10construct

Give $H \otimes K$ the algebra structure from [F3]. Define $Δ_{T} (h \otimes k) = \sum (h_{1} \otimes k_{1}) \otimes (h_{2} \otimes k_{2})$ , $ε_{T} (h \otimes k) = ε_{H} (h) ε_{K} (k)$ , and $S_{T} (h \otimes k) = S_{H} (h) \otimes S_{K} (k)$ ; these are the displayed maps with the middle factors flipped.

1.8givenF3F4F8F10algebra

For pure tensors, multiplicativity of the coproduct follows from $Δ_{T} ((h \otimes k) (h^{'} \otimes k^{'})) = \sum (h_{1} h_{1}^{'} \otimes k_{1} k_{1}^{'}) \otimes (h_{2} h_{2}^{'} \otimes k_{2} k_{2}^{'}) = Δ_{T} (h \otimes k) Δ_{T} (h^{'} \otimes k^{'})$ , using that $Δ_{H}, Δ_{K}$ are algebra maps and the tensor-product multiplication [F3, F4]. Unit preservation follows from $Δ_{H} (1) = 1 \otimes 1$ and $Δ_{K} (1) = 1 \otimes 1$ . Also $ε_{T} ((h \otimes k) (h^{'} \otimes k^{'})) = ε_{H} (h h^{'}) ε_{K} (k k^{'}) = ε_{T} (h \otimes k) ε_{T} (h^{'} \otimes k^{'})$ , and $ε_{T} (1_{H} \otimes 1_{K}) = 1$ , since both counits are unital algebra maps by [F4]. These equations extend linearly from pure tensors.

2.1step 1.1step 1.2step 1.3givenF1F3F4F5F6F8F9F10algebra

For $h, h^{'} \in H$ , $\overline{Δ} ((h + I) (h^{'} + I)) = (q_{I} \otimes q_{I}) Δ_{H} (h h^{'}) = (q_{I} \otimes q_{I}) (Δ_{H} (h) Δ_{H} (h^{'})) = \overline{Δ} (h + I) \overline{Δ} (h^{'} + I)$ , using that $Δ_{H}$ is an algebra map and [F3] gives the tensor-product algebra. Also $\overline{Δ} (1 + I) = (1 + I) \otimes (1 + I)$ , $\overline{ε} ((h + I) (h^{'} + I)) = ε_{H} (h) ε_{H} (h^{'})$ , and $\overline{ε} (1 + I) = 1$ , by [F4]. Coassociativity follows since the two composites on $h + I$ are respectively $(q_{I} \otimes q_{I} \otimes q_{I}) (Δ_{H} \otimes i d) Δ_{H} (h)$ and $(q_{I} \otimes q_{I} \otimes q_{I}) (i d \otimes Δ_{H}) Δ_{H} (h)$ , equal by coassociativity in $H$ ; the associators and tensor maps are natural by [F8]. The left counit composite on $h + I$ is $\sum \overline{ε} (h_{1} + I) (h_{2} + I) = \sum ε_{H} (h_{1}) (h_{2} + I) = h + I$ , and the right composite is $\sum (h_{1} + I) ε_{H} (h_{2}) = h + I$ , by the two counit equations in $H$ . For the left antipode equation, its value on $h + I$ is $\sum (S_{H} (h_{1}) + I) (h_{2} + I) = q_{I} (\sum S_{H} (h_{1}) h_{2}) = ε_{H} (h) (1 + I)$ ; the right equation is $\sum (h_{1} + I) (S_{H} (h_{2}) + I) = q_{I} (\sum h_{1} S_{H} (h_{2})) = ε_{H} (h) (1 + I)$ . Thus these maps make $H / I$ a Hopf algebra. Since $q_{I}$ is surjective and $q_{I} \otimes q_{I}$ is surjective (each elementary tensor of cosets has representatives and such tensors span), the quotient algebra and coalgebra maps are forced by $q_{I}$ ; the antipode is unique as a two-sided convolution inverse by [F5, F6].

2.2step 1.1step 1.2step 1.3step 1.4givenF2F4F8F9

If a Hopf map $f : H \to K$ kills $I$ , [F2] gives a unique algebra map $\overset{ˉ}{f} : H / I \to K$ with $\overset{ˉ}{f} q_{I} = f$ . Precomposing the coalgebra-map equation with $q_{I}$ gives $(\overset{ˉ}{f} \otimes \overset{ˉ}{f}) \overline{Δ} q_{I} = (f \otimes f) Δ_{H} = Δ_{K} f = Δ_{K} \overset{ˉ}{f} q_{I}$ ; surjectivity of $q_{I}$ proves the equation on $H / I$ . Counit preservation follows from $\overset{ˉ}{f} q_{I} = f$ and surjectivity of $q_{I}$ . For antipodes, $\overset{ˉ}{f} \overline{S} q_{I} = \overset{ˉ}{f} q_{I} S_{H} = f S_{H} = S_{K} f = S_{K} \overset{ˉ}{f} q_{I}$ by step 1.4; surjectivity of $q_{I}$ proves $\overset{ˉ}{f} \overline{S} = S_{K} \overset{ˉ}{f}$ . Thus $\overset{ˉ}{f}$ is a Hopf map.

2.3step 1.4step 1.5step 1.6F1algebra

By step 1.4, $S_{K} f = f S_{H}$ . Therefore for $j \in J$ , $f (S_{H} (j)) = S_{K} (f (j)) = S_{K} (0) = 0$ , so $S_{H} (J) \subseteq J$ . Together with steps 1.5 and 1.6, this says $J$ is a Hopf ideal.

2.4givenstep 1.7F4F8F10algebra

On $h \otimes k$ , the two iterated coproducts are $\sum (h_{11} \otimes k_{11}) \otimes (h_{12} \otimes k_{12}) \otimes (h_{2} \otimes k_{2})$ and $\sum (h_{1} \otimes k_{1}) \otimes (h_{21} \otimes k_{21}) \otimes (h_{22} \otimes k_{22})$ ; they agree by coassociativity in $H, K$ . Applying the left counit leg gives $\sum ε_{H} (h_{1}) ε_{K} (k_{1}) (h_{2} \otimes k_{2}) = h \otimes k$ ; applying the right leg gives $\sum (h_{1} \otimes k_{1}) ε_{H} (h_{2}) ε_{K} (k_{2}) = h \otimes k$ , by counitality in each factor. Thus $H \otimes K$ is a bialgebra.

3.1givenstep 1.7F7F9F10algebra∎

The left antipode product is $\sum (S_{H} (h_{1}) \otimes S_{K} (k_{1})) (h_{2} \otimes k_{2}) = ε_{H} (h) ε_{K} (k) (1_{H} \otimes 1_{K})$ , and the right product is $\sum (h_{1} \otimes k_{1}) (S_{H} (h_{2}) \otimes S_{K} (k_{2})) = ε_{H} (h) ε_{K} (k) (1_{H} \otimes 1_{K})$ . Each equality is the tensor product of the corresponding antipode identity in $H$ and $K$ , so $S_{T}$ is an antipode. The quotient and tensor-product constructions use no choice; AC is used only in the kernel tensor calculation through [F7].

Depends on

Used by

A tensor product Hopf algebra from a group and a primitive element Example

Cited to discharge well-definedness by Hopf ideals and Hopf subalgebras.

Dependency tree · two levels

42 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Andrew Baker, Hopf algebras over fields: an introduction, §§2.22–2.25 (standard reference, not scraped)