The largest Hopf ideal in a family of kernels #
Given morphisms f i : H ⟶ K i of commutative Hopf algebras, the ordinary intersection of
their ring-theoretic kernels need not come equipped with the structure of a Hopf ideal. This file
instead takes the supremum of all Hopf ideals contained in every kernel. The result is the largest
Hopf ideal through which every f i factors after quotienting H.
Contravariantly, this is the coordinate-algebra construction of the smallest closed subgroup
scheme containing a family of affine group-scheme morphisms into Spec H. In particular, it
forms the closed subgroup scheme generated by a family of Kostant root subgroups and a weight
torus.
Main declarations #
TauCeti.CommHopfAlgCat.commonKernelHopfIdeal: the largest Hopf ideal contained in all the kernels.TauCeti.CommHopfAlgCat.le_commonKernelHopfIdeal_iff: its universal property.TauCeti.CommHopfAlgCat.comapOfSurjective_commonKernelHopfIdeal: surjective pullback commutes with taking the common kernel of a family.TauCeti.CommHopfAlgCat.map_commonKernelHopfIdeal: an ambient isomorphism transports a common kernel to the common kernel of the transported family.TauCeti.CommHopfAlgCat.commonKernelHopfIdeal_eq_of_toIdeal_le_ker: members of the family that kill the common kernel of the others may be dropped.TauCeti.CommHopfAlgCat.comapOfSurjective_commonKernelHopfIdeal_le_of_comp_eq: an endomorphism that intertwines the family along a reindexing pulls the common-kernel ideal back into itself.TauCeti.CommHopfAlgCat.comapOfSurjective_commonKernelHopfIdeal_le_of_comp_eq_comp: the dependent-codomain version, allowing injective postcomposition maps.TauCeti.CommHopfAlgCat.commonKernelLift: the induced morphism from the quotient to each codomain.TauCeti.CommHopfAlgCat.commonKernelLift_surjective_of_surjective: a surjective member of the family remains surjective after factoring through the common-kernel quotient.TauCeti.CommHopfAlgCat.commonKernelHopfIdeal_eq_map_mkQuotient_of_comp: the common kernel of a family factored through a quotient is the image of its original common kernel.TauCeti.CommHopfAlgCat.commonKernelHopfIdeal_commonKernelLift_eq_bot: the quotient carries no further common kernel for the lifted family.
The largest Hopf ideal of H contained in the kernels of every morphism in f.
The supremum is taken in the complete upper semilattice of Hopf ideals. It is preferable to an ordinary intersection of kernels: no assertion that a ring-theoretic kernel is itself a Hopf ideal is needed.
Equations
- TauCeti.CommHopfAlgCat.commonKernelHopfIdeal f = sSup {I : TauCeti.HopfIdeal R ↑H | ∀ (i : ι), I.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (f i))).toRingHom}
Instances For
The common-kernel Hopf ideal is contained in the kernel of each member of the family.
A Hopf ideal lies below the common-kernel ideal exactly when every morphism kills it.
Pulling a common-kernel Hopf ideal back along a surjective ambient morphism gives the common kernel of the precomposed family.
An ambient isomorphism carries a common-kernel Hopf ideal to the common kernel of the family precomposed with its inverse.
Dropping redundant members of a family. If every member indexed by κ kills the
common-kernel ideal of the members indexed by ι, then adjoining them does not change the
common-kernel ideal.
Contravariantly, generators whose images already lie in the closed subgroup scheme generated by the others may be dropped.
An endomorphism which intertwines a family up to injective maps of the codomains pulls the
common-kernel ideal back into itself. This is the version of
comapOfSurjective_commonKernelHopfIdeal_le_of_comp_eq for a dependent family of codomains and
commuting squares φ ≫ f (s i) = f i ≫ m i. Injectivity of m i is exactly what lets vanishing
after postcomposition imply vanishing under f i.
An endomorphism that intertwines the family along a reindexing pulls the common-kernel ideal
back into itself. If every f i factors as φ followed by some other member f (s i) of the
family, then the inverse image of the common-kernel ideal along φ is again contained in it.
The conclusion is one containment, not invariance: an automorphism fixing the ideal needs this lemma once for itself and once for its inverse.
The reindexing s is an arbitrary function ι → ι; at s = id the hypothesis reads φ ≫ f i = f i, so the statement specialises to an endomorphism fixing the family pointwise.
The morphism from the common-kernel quotient induced by the ith member of the family.
Equations
Instances For
The quotient morphism followed by a common-kernel lift is the original morphism.
A surjective member of a family remains surjective after factoring through the common-kernel quotient. Equivalently, its contravariant map of affine group schemes remains a closed immersion after the target is replaced by the closed subgroup generated by the family.
A morphism from the common-kernel quotient is determined by its composite with the quotient morphism.
If a family of Hopf-algebra morphisms factors through H ⟶ H ⧸ I, then its common
kernel after quotienting is the image of its original common kernel in H ⧸ I.
This identifies the defining Hopf ideal of the same generated closed subgroup when the ambient affine group scheme is replaced by a quotient containing it.
The common-kernel quotient carries no further common kernel: the lifted family separates it.
Contravariantly, the closed subgroup scheme generated by a family of morphisms is generated by their factorizations through it.