complex conjugation

Stream: Is there code for X?

[Kevin Buzzard]

I assume we have complex conjugation as an $\R$-algebra map on $\mathbb{C}$? I don't know how to search for this; #loogle ℂ →ₐ[ℝ] ℂ gives no results (am I using it correctly?) and by exact? gives me the identity map. I actually want a more abstract complex conjugation but I can get it from the one on the complexes.

import Mathlib

-- is this missing?
instance : IsAlgClosure ℝ ℂ where
  isAlgClosed := Complex.isAlgClosed
  isAlgebraic := Algebra.IsAlgebraic.of_finite ℝ ℂ

-- is this something to do with `star`?
example : ℂ →ₐ[ℝ] ℂ := sorry

#loogle ℂ →ₐ[ℝ] ℂ

-- Not hard to make this if we have the above.
def Complex.complex_conjugation : Gal(ℂ / ℝ) := sorry

open Field

-- what I actually want
noncomputable def Real.absoluteGaloisGroup_complex_conjugation :
    absoluteGaloisGroup ℝ :=
  (IsAlgClosure.equiv ℝ ℂ (AlgebraicClosure ℝ)).autCongr Complex.complex_conjugation

-- I also want that it has order 2, but let's get a definition first :-)

[Riccardo Brasca]

Complex.conjAe

[Riccardo Brasca]

This is why I wanted a CM-field instance (that doesn't hold unfortunately) on ℂ.

[Riccardo Brasca]

Anyway, the point is that ℂ is a StarSomething

[Riccardo Brasca]

Note that we have a good API for "complex conjugations" as in NumberField.ComplexEmbedding.IsConj

[Kevin Buzzard]

Annoyingly #loogle ℂ ≃ₐ[ℝ] ℂ doesn't find docs#Complex.conjAe either :-( (and neither does #loogle Gal(ℂ/ℝ)).

Ha ha example : Gal(ℂ/ℝ) := by exact? finds it :-)

Thanks anyway! Yeah we have IsComplexConjugate but sometimes it's useful to have complexConjugate as well (in some stupid generality).

[Jireh Loreaux]

@loogle ⊢ ?k ≃ₐ[ℝ] ?k

[loogle]

:search: RCLike.conjAe, Complex.conjAe

[Jireh Loreaux]

I can't explain why instantiating with ?k with ℂ fails.

[Eric Wieser]

It looks like it's doing a syntactic match on the found instance

[Jireh Loreaux]

ouch, that seems like a big paper cut.

[Eric Wieser]

@loogle @AlgEquiv ℝ ℂ ℂ

[loogle]

:search: Complex.conjAe, Complex.conjAe_coe, and 2 more

[Kevin Buzzard]

Remark: Loogle discovering RCLike.conjAe makes me want to comment that this is a situation where we could have the more general IsROrC.conjAe where we don't choose a square root of -1. I used to bang on about this a lot but I've since realised that actually I don't want IsROrC for Langlands, I want IsC, and we have this now: it's IsAlgClosure \R K (which ironically we don't seem to have for $\mathbb{C}$ ;-) )

[Eric Wieser]

I think your proposed IsROrC for Real probably ought to choose a square root of -1 (as 0 to match Real.sqrt)

[Kenny Lau]

we only have 33 lemmas on IsAlgClosure, but we have the components already:

import Mathlib

instance : IsAlgClosure ℝ ℂ := .mk inferInstance inferInstance

#min_imports

(and I suppose in practice it's the components that you want to use)

[Kevin Buzzard]

Well, I wanted to use IsAlgClosure.equiv (as you can see) which needed the instance.

[Kevin Buzzard]

Eric Wieser said:

I think your proposed IsROrC for Real probably ought to choose a square root of -1 (as 0 to match Real.sqrt)

The point about IsROrC is that it is a Prop (we used to have one which wasn't a Prop, which drove me nuts, but now it's RCLike). But I since realised that I only want it for $\R$-algebras and actually I know exactly when they're $\R$ and when they're isomorphic to $\mathbb{C}$ which is why IsAlgClosure is perfect (I really just want IsR and IsC so that they can be applied to completions of number fields).