The category of algebraic function fields

For a field k, the algebraic function fields of one variable over k (fields F with a k-algebra structure satisfying TauCeti.IsFunctionField k F) form a category whose morphisms are the k-algebra homomorphisms. Every such homomorphism is injective, so the morphisms are the k-embeddings of function fields. This is the field side of the anti-equivalence between algebraic function fields of one variable over k and regular proper curves over k.

The bundled objects and the morphism structure follow Mathlib's AlgCat.

Main definitions

• TauCeti.FunctionFieldCat k: the category of algebraic function fields over k.
• TauCeti.FunctionFieldCat.of: the object of FunctionFieldCat k given by a function field.
• TauCeti.FunctionFieldCat.Hom.hom and TauCeti.FunctionFieldCat.ofHom: the passage between morphisms of FunctionFieldCat k and k-algebra homomorphisms.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Appendix B.

structure TauCeti.FunctionFieldCat (k : Type u) [Field k] : Type (u + 1)

The category of algebraic function fields of one variable over a field k: fields F with a k-algebra structure satisfying IsFunctionField k F, with k-algebra homomorphisms as morphisms.

• carrier : Type u

  The underlying field.

• field : Field ↑self
• algebra : Algebra k ↑self
• isFunctionField : IsFunctionField k ↑self

  The underlying field is an algebraic function field over k.

@[instance_reducible]

instance TauCeti.FunctionFieldCat.instCoeSortType {k : Type u} [Field k] : CoeSort (FunctionFieldCat k) (Type u)

@[reducible, inline]

abbrev TauCeti.FunctionFieldCat.of {k : Type u} [Field k] (F : Type u) [Field F] [Algebra k F] (hF : IsFunctionField k F) : FunctionFieldCat k

The object of FunctionFieldCat k given by an algebraic function field F over k.

theorem TauCeti.FunctionFieldCat.coe_of {k : Type u} [Field k] (F : Type u) [Field F] [Algebra k F] (hF : IsFunctionField k F) : ↑(of F hF) = F

structure TauCeti.FunctionFieldCat.Hom {k : Type u} [Field k] (F G : FunctionFieldCat k) : Type u

The type of morphisms in FunctionFieldCat k.

• hom' : ↑F →ₐ[k] ↑G

  The underlying k-algebra homomorphism.

theorem TauCeti.FunctionFieldCat.Hom.ext {k : Type u} {inst✝ : Field k} {F G : FunctionFieldCat k} {x y : F.Hom G} (hom' : x.hom' = y.hom') : x = y

theorem TauCeti.FunctionFieldCat.Hom.ext_iff {k : Type u} {inst✝ : Field k} {F G : FunctionFieldCat k} {x y : F.Hom G} : x = y ↔ x.hom' = y.hom'

@[instance_reducible]

instance TauCeti.FunctionFieldCat.instCategory {k : Type u} [Field k] : CategoryTheory.Category.{u, u + 1} (FunctionFieldCat k)

@[instance_reducible]

instance TauCeti.FunctionFieldCat.instConcreteCategoryAlgHomCarrier {k : Type u} [Field k] : CategoryTheory.ConcreteCategory (FunctionFieldCat k) fun (x1 x2 : FunctionFieldCat k) => ↑x1 →ₐ[k] ↑x2

@[reducible, inline]

abbrev TauCeti.FunctionFieldCat.Hom.hom {k : Type u} [Field k] {F G : FunctionFieldCat k} (f : F.Hom G) : ↑F →ₐ[k] ↑G

The k-algebra homomorphism underlying a morphism of FunctionFieldCat k.

@[reducible, inline]

abbrev TauCeti.FunctionFieldCat.ofHom {k : Type u} [Field k] {F G : FunctionFieldCat k} (f : ↑F →ₐ[k] ↑G) : F ⟶ G

The morphism of FunctionFieldCat k given by a k-algebra homomorphism.

def TauCeti.FunctionFieldCat.Hom.Simps.hom {k : Type u} [Field k] (F G : FunctionFieldCat k) (f : F.Hom G) : ↑F →ₐ[k] ↑G

Use the ConcreteCategory.hom projection for @[simps] lemmas.

@[simp]

theorem TauCeti.FunctionFieldCat.hom_id {k : Type u} [Field k] {F : FunctionFieldCat k} : Hom.hom (CategoryTheory.CategoryStruct.id F) = AlgHom.id k ↑F

@[simp]

theorem TauCeti.FunctionFieldCat.hom_comp {k : Type u} [Field k] {F G H : FunctionFieldCat k} (f : F ⟶ G) (g : G ⟶ H) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

theorem TauCeti.FunctionFieldCat.hom_ext {k : Type u} [Field k] {F G : FunctionFieldCat k} {f g : F ⟶ G} (h : Hom.hom f = Hom.hom g) : f = g

theorem TauCeti.FunctionFieldCat.hom_ext_iff {k : Type u} [Field k] {F G : FunctionFieldCat k} {f g : F ⟶ G} : f = g ↔ Hom.hom f = Hom.hom g

@[simp]

theorem TauCeti.FunctionFieldCat.hom_ofHom {k : Type u} [Field k] {F G : FunctionFieldCat k} (f : ↑F →ₐ[k] ↑G) : Hom.hom (ofHom f) = f

@[simp]

theorem TauCeti.FunctionFieldCat.ofHom_hom {k : Type u} [Field k] {F G : FunctionFieldCat k} (f : F ⟶ G) : ofHom (Hom.hom f) = f

@[simp]

theorem TauCeti.FunctionFieldCat.ofHom_id {k : Type u} [Field k] {F : FunctionFieldCat k} : ofHom (AlgHom.id k ↑F) = CategoryTheory.CategoryStruct.id F

@[simp]

theorem TauCeti.FunctionFieldCat.ofHom_comp {k : Type u} [Field k] {F G H : FunctionFieldCat k} (f : ↑F →ₐ[k] ↑G) (g : ↑G →ₐ[k] ↑H) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

def TauCeti.FunctionFieldCat.isoMk {k : Type u} [Field k] {F G : FunctionFieldCat k} (e : ↑F ≃ₐ[k] ↑G) : F ≅ G

An isomorphism of FunctionFieldCat k from a k-algebra isomorphism.

@[simp]

theorem TauCeti.FunctionFieldCat.isoMk_hom {k : Type u} [Field k] {F G : FunctionFieldCat k} (e : ↑F ≃ₐ[k] ↑G) : (isoMk e).hom = ofHom ↑e

@[simp]

theorem TauCeti.FunctionFieldCat.isoMk_inv {k : Type u} [Field k] {F G : FunctionFieldCat k} (e : ↑F ≃ₐ[k] ↑G) : (isoMk e).inv = ofHom ↑e.symm