subfields

Stream: maths

[Johan Commelin]

I was thinking a bit about central simple algebras. One fact that is quite useful is the following:

Let $D$ be a finite-dimensional central division algebra over a field $K$. Then every maximal subfield $E$ of $D$ contains $K$ and $\dim_K(D) = \dim_K(E)^2 = n^2$. Moreover, $E \otimes_K D \cong \text{Mat}_n(E)$.

Example: take the quaternions $\mathbb H$ over $\R$. They contain $\R(i) \cong \mathbb C$ as subfield. And indeed, $\dim(\mathbb H) = 4 = 2^2 = \dim(\mathbb C)^2$.

[Johan Commelin]

This lemma suggests that subfield should be defined for rings R that are not necessary fields.

[Johan Commelin]

Currently docs#subfield is only defined for fields. What would be the best general context to talk about subfields?

[Johan Commelin]

Mathematically, any semiring can have a subfield. But those don't always come with a has_inv. And I can imagine that we want a quasi-computable inverse for these subfields.

[Scott Morrison]

Monoid objects in linear monoidal categories? :-) (10% serious.)

[Johan Commelin]

Should subfield R be defined for [semiring R] [has_inv R]?

[Johan Commelin]

It would need extra axioms beyond what it has now, to ensure that the carrier set really is a subfield.

[Johan Commelin]

Currently we have

/-- `subfield R` is the type of subfields of `R`. A subfield of `R` is a subset `s` that is a
  multiplicative submonoid and an additive subgroup. Note in particular that it shares the
  same 0 and 1 as R. -/
structure subfield (K : Type u) [field K] extends subring K :=
(inv_mem' : ∀ x ∈ carrier, x⁻¹ ∈ carrier)

[Johan Commelin]

That docstring also seems wrong... it doesn't mention multiplicative inverses at all :see_no_evil:

[Johan Commelin]

Just thinking out loud. How about something like (I didn't test this code):

/-- `subfield R` is the type of subfields of `R`. A subfield of `R` is a subset `s` that is
  an additive subgroup and a multiplicative submonoid,
  and such that every nonzero element has a multiplicative inverse.
  Note in particular that it shares the same `0` and `1` as `R`. -/
structure subfield (R : Type u) [ring R] [has_inv R] extends subring R :=
(inv_mem' : ∀ x ∈ carrier, x⁻¹ ∈ carrier)
(inv_mul_self' : ∀ x ∈ carrier, x \ne 0 -> x⁻¹ * x = 1)
(self_mul_inv' : ∀ x ∈ carrier, x \ne 0 -> x * x⁻¹ = 1)

def subfield.mk' {R : Type*} [division_ring R] (S : subring R) (h : ∀ x ∈ S, x⁻¹ ∈ S) :
  subfield R :=
{ inv_mem' := h,
  inv_mul_self' := by { intros, simp [*] },
  self_mul_inv' := by { intros, simp [*] },
  .. S }

[Anne Baanen]

0 should also be a member of the subfield, no?

[Johan Commelin]

extends subring R takes care of that, right?

[Anne Baanen]

Well, inv_mul_self 0 is false currently :P

[Johan Commelin]

ooh, lol. I need a x \ne 0 assumption.

[Johan Commelin]

Also, I guess semiring doesn't give me a has_sub :face_palm: so we need to deal with that as well.

[Johan Commelin]

Probably assuming that the ambient structure is a ring is not a problem in practice

[Anne Baanen]

Overall, this seems like a good idea, Also for reasons of speeding up some big unification chains we get when adjoining elements to a complicated field.

[Johan Commelin]

ooh, I'm also missing a mul_comm assumption :face_palm:

[Anne Baanen]

What if we tried putting the missing operators in a field of the structure?

/-- `subfield R` is the type of subfields of `R`. A subfield of `R` is a subset `s` that is
  an additive subgroup and a multiplicative submonoid,
  and such that every nonzero element has a multiplicative inverse.
  Note in particular that it shares the same `0` and `1` as `R`. -/
structure subfield (R : Type u) [semiring R] extends subring R :=
(neg : carrier → carrier)
(inv : carrier → carrier)
(inv_mul_self' : ∀ x ≠ 0, inv x * x = 1)
(self_mul_inv' : ∀ x ≠ 0, x * inv x = 1)

[Johan Commelin]

Then it's no longer set_like, is it?

[Johan Commelin]

Ooh it should be, given the right axioms on that data.

[Anne Baanen]

We could even drop the 0 and 1 and just assume has_add and has_mul, but that would be too much :P

[Adam Topaz]

What happens if I want to talk about $\mathbb{Q}[\sqrt{2}]$ as a subfield of $\mathbb{Q}[X,Y]/(X^2-2)$?

[Adam Topaz]

I think the [has_inv R] is an issue.

[Adam Topaz]

Oh yeah, Anne's suggestion would take care of this ;)

[Johan Commelin]

Should we do the same with subgroup, so that we can talk about subgroups of monoids, etc, etc...?

[Adam Topaz]

ughh

[Johan Commelin]

I guess subfield (and subdivision_ring) are maybe the ones that really matter in practice. (E.g. the example that you gave.)

[Adam Topaz]

Do we really want to go through all this trouble? Why can't we just use injective morphisms from a field to the semiring?

[Eric Wieser]

We solved this for monoids with submonoid (units M), right?

[Johan Commelin]

Do you mean subgroup (units M)?

[Adam Topaz]

?? Isn't that the type of subgroups of units M?

[Adam Topaz]

(Which is already a group)

[Johan Commelin]

Right, but every subgroup of a monoid M is a subgroup of units M, at least for a mathematicians version of "is".

[Adam Topaz]

But this doesn't hold for subfields of a (semi)ring

[Adam Topaz]

(I think?)

[Adam Topaz]

E.g. $k(t) \otimes_k k(s)$ where $k$ is a field has both $k(s)$ and $k(t)$ as subfields, but not $k(s,t)$.

[Eric Wieser]

Yeah, I don't know if there's an analogous construction for subfields, I brought it up in response to the mention of subgroups above.

[Kevin Buzzard]

Adam Topaz said:

E.g. $k(t) \otimes_k k(s)$ where $k$ is a field and $s,t$ are both variables has both $k(s)$ and $k(t)$ as subfields, but not $k(s,t)$.

I agree -- I guess the tensor product is the localisation of $k[s,t]$ at the submonoid generated by $s$ and $t$.

[Kevin Buzzard]

How about defining subfield for division rings? Where else do we take maximal subfields?

[Adam Topaz]

Sure, that's what Johan originally was asking about, but I think it's worthwhile to come up with an idea that will work for arbitrary semirings.

[Kevin Buzzard]

But division rings will have a div and semirings don't? What is an example in real life where we demand a div on a subobject of an object which doesn't have a div?

[Eric Wieser]

Relaxing field to division_ring in subfield should be trivial, shouldn't it?

[Kevin Buzzard]

that was why I was mentioning it!

[Kevin Buzzard]

It seems to be a very simple solution in the case in hand, and we can just kick the harder question down the road in the hope that nobody ever needs it :-)

[Adam Topaz]

In real life fields don't have an inv, because they're defined as rings satisfying certain (prop-valued) axioms (for a similar reason, fields don't form a variety in the sense of universal algebra), so I can freely say that $\mathbb{Q}$ is a subfield of $\mathbb{Q}[X]$, even though $\mathbb{Q}[X]$ has no division operation.

[Johan Commelin]

Yup, and I think we should support that use case

[Kevin Buzzard]

I'm just remarking that it seems harder and although we all know that it could in theory be necessary, nobody came up with a real life example. Galois theory uses subfields and the central simple algebra theory uses division rings.

[Eric Wieser]

In general I suppose a common subfield of a non-division_ring is (algebra_map K A).range?

[Eric Wieser]

Which isn't to say there's anything particularly interesting about that subfield, but it's easy to construct

[Johan Commelin]

I'll make a PR that generalizes to division rings. We can always generalize further at a later point.

[Kevin Buzzard]

Actually, aren't there theorems about maximal subfields of matrix rings? :P

Remember that an integral domain finite-dimensional over a field is a a field, so in e.g. the matrix case you're looking for subfields of M_n(K) which contain K and for this you can just use commutative subrings containing K.

[Johan Commelin]

#8901

[Eric Wieser]

I was expecting the generalization to sub-division_rings, since sub-division_rings of a field are automatically subfields. To my surprise, the PR actually does require commutativity within the subfield. I commented there, but here seems like a better place to discuss.

Do we actually need to talk about commutative subfields of divisionrings? We seem to have survived just fine without commutative submonoids of non-commutative monoids, commutative subgroups of non-commutative groups, etc...

[Eric Wieser]

(and by just fine; I mean I remember only one Zulip thread about commutative subgroups, but am on mobile so would be unable to link it if I could find it)

[Adam Topaz]

For reference: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Abelian.20Subgroup/near/242371758

[Eric Wieser]

One option would be something like:

class set_like.commutative {A B} [set_like A B] [has_mul A] (S : B) :=
(mul_comm : ∀ x y ∈ S, x * y = y * x)

And then use this to provide more general versions of docs#subfield.to_field, docs#subgroup.to_comm_group, and docs#submonoid.to_comm_monoid and similarly for the additive versions; all of which don't require commutativity of the base type, and only within the subtype.

[Johan Commelin]

@Eric Wieser I think we want to be able to talk about maximal subfields of division rings. That's easy with the current approach, because you can simply talk about maximal elements in the lattice subfield K.

[Johan Commelin]

quaternion algebras over $\mathbb Q$ contain fields that are degree 2 over $\mathbb Q$.

[Johan Commelin]

Those fields are actually quite interesting.

[Eric Wieser]

Hmm, I guess otherwise you have to put a lattice structure on { S : subdivision_ring K // set_like.is_commutative S } which is straightforward but annoying.

[Eric Wieser]

My main objection to your approach is it opens the doors to also adding sub_(add_)comm_monoid and sub_(add_)group and monoid_hom.crange and monoid_hom.mcrange and ...

[Eric Wieser]

That is, it appears to scale poorly. But perhaps all the things that it could potentially scale to are mathematically entirely uninteresting.

[Johan Commelin]

Yeah, I agree with that point. I don't have a lot of evidence that subfields should be a special case.

[Johan Commelin]

Currently #8901 doesn't build. Before fixing it, I think it would be good to reach a concensus about what we want the definition of subfield to be. I claim they should be commutative.

[Notification Bot]

This topic was moved by Johan Commelin to #new members > Elham Mazaheri