From 9da39836ecc46b2893f38bcd7937be262bb9b67c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 25 Jul 2024 15:06:26 +0300 Subject: [PATCH] footnotes --- posts/tradeoff-of-defining-types-as-subobjects.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/posts/tradeoff-of-defining-types-as-subobjects.md b/posts/tradeoff-of-defining-types-as-subobjects.md index 4d0fb1b2..cd0d2597 100644 --- a/posts/tradeoff-of-defining-types-as-subobjects.md +++ b/posts/tradeoff-of-defining-types-as-subobjects.md @@ -11,7 +11,7 @@ title: Tradeoffs of defining types as subobjects type: text --- -It often happens in formalisation that a type of interest is a subobject of another type of interest. For example, the unit circle in the complex plane is naturally a submonoid (nevermind that it is actually a subgroup, we currently can't talk about subgroups of fields). +It often happens in formalisation that a type of interest is a subobject of another type of interest. For example, the unit circle in the complex plane is naturally a submonoid[^1]. What is the best way of defining this unit circle in terms of `Complex`? This blog post examines the pros and cons of the available designs. @@ -116,4 +116,7 @@ Subobjects are not the only ones having a coercion to `Type`: Concrete categorie For example, [`AlgebraicGeometry.Scheme`](https://leanprover-community.github.io/mathlib4_docs/find/?pattern=AlgebraicGeometry.Scheme#doc) sees widespread use in algebraic geometry and [`AlgebraicGeometry.Proj`](https://leanprover-community.github.io/mathlib4_docs/find/?pattern=AlgebraicGeometry.Proj#doc) is a term of type `Scheme` that is also used as a type. -This raises issues of its own, as `Proj 𝒜` is (mathematically) also a smooth manifold for some graded algebras `𝒜`. Since terms only have one type, we can't hope to have both `Proj 𝒜 : Scheme` and `Proj 𝒜 : SmoothMnfld` (this last category does not exist yet in Mathlib). One option would be to have a separate `DifferentialGeometry.Proj 𝒜` of type `SmoothMnfld`. Another one would be to provide the instances saying that `AlgebraicGeometry.Proj 𝒜` is a smooth manifold. \ No newline at end of file +This raises issues of its own, as `Proj 𝒜` is (mathematically) also a smooth manifold for some graded algebras `𝒜`. Since terms only have one type, we can't hope to have both `Proj 𝒜 : Scheme` and `Proj 𝒜 : SmoothMnfld`[^2]. One option would be to have a separate `DifferentialGeometry.Proj 𝒜` of type `SmoothMnfld`. Another one would be to provide the instances saying that `AlgebraicGeometry.Proj 𝒜` is a smooth manifold. + +[^1]: Nevermind that it is actually a subgroup. Mathlib currently can't talk about subgroups of fields. +[^2]: The `SmoothMnfld` category does not exist yet in Mathlib \ No newline at end of file