Infrastructure for Hopf spectra

This file computes the underlying scheme maps of Mathlib's AlgebraicGeometry.hopfSpec on an arbitrary same-universe commutative Hopf algebra. It identifies the underlying scheme with the ordinary spectrum, the structural morphism with the algebra structure map, the multiplication source with the standard affine fibre product, and the group operations with the counit, comultiplication, and antipode.

It also records coordinate equality and extensionality lemmas obtained from the full faithfulness of hopfSpec.

These lemmas provide the common projection boundary used by concrete affine group schemes. The same-universe restriction is inherited from Mathlib's current hopfSpec construction.

Main declarations

• TauCeti.hopfSpec_obj_X_left: the underlying scheme of a Hopf spectrum.
• TauCeti.hopfSpec_obj_X_hom: its structural morphism.
• TauCeti.hopfSpec_obj_eq_asOver: its bundled identification with the group object on the ordinary spectrum.
• TauCeti.hopfSpec_obj_tensor_X_left: the source of its multiplication.
• TauCeti.algSpec_map_left_ofAlgHom: the underlying spectrum map of an algebra morphism.
• TauCeti.hopfSpec_obj_one_left, TauCeti.hopfSpec_obj_mul_left, and TauCeti.hopfSpec_obj_inv_left: its three group operations.
• CommHopfAlgCat.preimage_unop_comp_eq_of_hopfSpec_map_comp_eq and CommHopfAlgCat.hom_ext_of_preimage_unop_eq: coordinate equalities and extensionality transported through the full faithfulness of hopfSpec.
• TauCeti.isCocomm_iff_isCommMonObj_hopfSpec: cocommutativity corresponds to a commutative group object.
• TauCeti.instIsCommMonObjHopfSpec: a cocommutative Hopf algebra has a commutative Hopf spectrum.
• TauCeti.moduleFinite_iff_isFinite_hopfSpec: module-finiteness corresponds to a finite structural morphism.
• TauCeti.moduleFlat_iff_flat_hopfSpec: module-flatness corresponds to a flat structural morphism.
• TauCeti.algebraFinitePresentation_iff_locallyOfFinitePresentation_hopfSpec: finite presentation of an algebra corresponds to local finite presentation of its structural morphism.
• TauCeti.moduleProjective_iff_flat_and_finitePresentation: a finite algebra is projective as a module exactly when it is flat and finitely presented as an algebra.
• TauCeti.moduleProjective_iff_flat_and_locallyOfFinitePresentation_hopfSpec: the corresponding characterization in terms of the structural morphism of a Hopf spectrum.
• TauCeti.finrank_hopfSpec: the rank function of a finite flat Hopf spectrum is the local rank of its coordinate algebra.

theorem CommHopfAlgCat.preimage_unop_comp_eq_of_hopfSpec_map_comp_eq {R : Type u} [CommRing R] {K Y Q : CommHopfAlgCat R} (c : Q ⟶ K) (φ ψ : (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op Q) ⟶ (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op Y)) (hc : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map c.op) φ = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map c.op) ψ) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.hopfSpec.fullyFaithful.preimage φ).unop c = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.hopfSpec.fullyFaithful.preimage ψ).unop c

Coordinate equalities transport through hopfSpec, one map at a time. If two homomorphisms of affine group schemes out of Spec Q agree after composing with the homomorphism represented by a coordinate morphism c : Q ⟶ K, then their coordinate preimages agree after composing with c.

theorem CommHopfAlgCat.hom_ext_of_preimage_unop_eq {R : Type u} [CommRing R] {Y Q : CommHopfAlgCat R} (φ ψ : (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op Q) ⟶ (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op Y)) (h : (AlgebraicGeometry.hopfSpec.fullyFaithful.preimage φ).unop = (AlgebraicGeometry.hopfSpec.fullyFaithful.preimage ψ).unop) : φ = ψ

Coordinate extensionality transports through hopfSpec. Two homomorphisms of affine group schemes between Hopf spectra are equal as soon as their coordinate preimages are.

instance TauCeti.isFinite_respectsIso : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.IsFinite

Finite morphisms of schemes respect isomorphisms.

instance TauCeti.flat_respectsIso : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.Flat

Flat morphisms of schemes respect isomorphisms.

instance TauCeti.locallyOfFinitePresentation_respectsIso : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.LocallyOfFinitePresentation

Morphisms of schemes locally of finite presentation respect isomorphisms.

@[simp]

theorem TauCeti.hopfSpec_obj_X_left (R : Type u) [CommRing R] (H : CommHopfAlgCat R) : ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)).X.left = AlgebraicGeometry.Spec ↧↑H

The scheme underlying the Hopf spectrum of H is its ordinary spectrum.

@[simp]

theorem TauCeti.hopfSpec_obj_X_hom (R : Type u) [CommRing R] (H : CommHopfAlgCat R) : ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)).X.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R ↑H)))

The structural morphism of a Hopf spectrum is induced by its algebra structure map.

theorem TauCeti.morphismProperty_hopfSpec_obj_X_hom_iff (R : Type u) [CommRing R] (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [P.RespectsIso] (H : CommHopfAlgCat R) : P ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)).X.hom ↔ P (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R ↑H)))

A morphism property that respects isomorphisms holds for the structural morphism of a Hopf spectrum exactly when it holds for the spectrum map induced by the algebra structure map.

@[simp]

theorem TauCeti.hopfSpec_obj_tensor_X_left (R : Type u) [CommRing R] (H : CommHopfAlgCat R) : (CategoryTheory.MonoidalCategoryStruct.tensorObj ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)).X ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)).X).left = CategoryTheory.Limits.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R ↑H))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R ↑H)))

The multiplication source of a Hopf spectrum is the standard affine fibre product of two copies of its underlying spectrum over the base.

@[simp]

theorem TauCeti.algSpec_map_left_ofAlgHom (R : Type u) [CommRing R] {A B : Type u} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) : CategoryTheory.Over.Hom.left ((AlgebraicGeometry.algSpec ↧R).map (CommAlgCat.ofHom f).op) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑f)

Applying algSpec to an algebra homomorphism has underlying scheme map Spec.map of its underlying ring homomorphism.

Mathlib's algSpec_map_left leaves this map expressed through the CommAlgCat/under-category equivalence, and no public computation lemma exposes the resulting Under.Hom.right. The final reduction is therefore definitional and is localized here.

theorem TauCeti.hopfSpec_obj_eq_asOver (R : Type u) [CommRing R] (H : CommHopfAlgCat R) : (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H) = { X := (AlgebraicGeometry.Spec ↧↑H).asOver (AlgebraicGeometry.Spec ↧R), grp := AlgebraicGeometry.instGrpObjSpecAsOverSpec }

Mathlib's hopfSpec object is the group object on the ordinary spectrum.

This bundled identification carries the group structure across the two instance paths. Mathlib's operation computation lemmas are stated for (Spec H).asOver (Spec R), while hopfSpec reaches that group object through the Hopf-algebra/cogroup equivalence.

@[simp]

theorem TauCeti.hopfSpec_obj_one_left (R : Type u) [CommRing R] (H : CommHopfAlgCat R) : CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(Bialgebra.counitAlgHom R ↑H))) (CategoryTheory.eqToHom ⋯)

The unit of a Hopf spectrum is induced by the counit of its coordinate Hopf algebra.

@[simp]

theorem TauCeti.hopfSpec_obj_mul_left (R : Type u) [CommRing R] (H : CommHopfAlgCat R) : CategoryTheory.Over.Hom.left CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R ↑H ↑H).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(Bialgebra.comulAlgHom R ↑H))) (CategoryTheory.eqToHom ⋯)))

Multiplication on a Hopf spectrum is induced by the comultiplication of its coordinate Hopf algebra.

@[simp]

theorem TauCeti.hopfSpec_obj_inv_left (R : Type u) [CommRing R] (H : CommHopfAlgCat R) : CategoryTheory.Over.Hom.left CategoryTheory.GrpObj.inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(HopfAlgebra.antipodeAlgHom R ↑H))) (CategoryTheory.eqToHom ⋯))

Inversion on a Hopf spectrum is induced by the antipode of its coordinate Hopf algebra.

theorem TauCeti.isCocomm_iff_isCommMonObj_hopfSpec (R : Type u) [CommRing R] (H : CommHopfAlgCat R) : Coalgebra.IsCocomm R ↑H ↔ CategoryTheory.IsCommMonObj ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)).X

A Hopf spectrum is a commutative group object exactly when its coordinate Hopf algebra is cocommutative.

instance TauCeti.instIsCommMonObjHopfSpec (R : Type u) [CommRing R] (H : CommHopfAlgCat R) [Coalgebra.IsCocomm R ↑H] : CategoryTheory.IsCommMonObj ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)).X

The Hopf spectrum of a cocommutative Hopf algebra is a commutative group object.

theorem TauCeti.moduleFinite_iff_isFinite_hopfSpec (R : Type u) [CommRing R] (H : CommHopfAlgCat R) : Module.Finite R ↑H ↔ AlgebraicGeometry.IsFinite ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)).X.hom

A Hopf spectrum is finite over its base exactly when its coordinate algebra is module-finite.

theorem TauCeti.moduleFlat_iff_flat_hopfSpec (R : Type u) [CommRing R] (H : CommHopfAlgCat R) : Module.Flat R ↑H ↔ AlgebraicGeometry.Flat ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)).X.hom

A Hopf spectrum is flat over its base exactly when its coordinate algebra is flat as a module.

theorem TauCeti.algebraFinitePresentation_iff_locallyOfFinitePresentation_hopfSpec (R : Type u) [CommRing R] (H : CommHopfAlgCat R) : Algebra.FinitePresentation R ↑H ↔ AlgebraicGeometry.LocallyOfFinitePresentation ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)).X.hom

A Hopf spectrum is locally of finite presentation over its base exactly when its coordinate algebra is finitely presented.

theorem TauCeti.moduleProjective_iff_flat_and_finitePresentation (R A : Type u) [CommRing R] [CommRing A] [Algebra R A] [Module.Finite R A] : Module.Projective R A ↔ Module.Flat R A ∧ Algebra.FinitePresentation R A

A finite commutative algebra is projective as a module exactly when it is flat as a module and finitely presented as an algebra.

theorem TauCeti.moduleProjective_iff_flat_and_locallyOfFinitePresentation_hopfSpec (R : Type u) [CommRing R] (H : CommHopfAlgCat R) [Module.Finite R ↑H] : Module.Projective R ↑H ↔ AlgebraicGeometry.Flat ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)).X.hom ∧ AlgebraicGeometry.LocallyOfFinitePresentation ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)).X.hom

For a finite Hopf algebra over a commutative ring, projectivity of the coordinate algebra is equivalent to flatness and local finite presentation of its Hopf spectrum over the base.

@[simp]

theorem TauCeti.finrank_hopfSpec (R : Type u) [CommRing R] (H : CommHopfAlgCat R) [Module.Finite R ↑H] [Module.Flat R ↑H] (x : PrimeSpectrum R) : AlgebraicGeometry.Scheme.Hom.finrank ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)).X.hom x = Module.rankAtStalk (↑H) x

The rank function of a finite flat Hopf spectrum is the local rank of its coordinate algebra.