## Stream: general

### Topic: Group morphism

#### orlando (Mar 26 2020 at 21:54):

Hello,

I have a little problem, it's just computation but i can't do !!! Is there a tatict how deal with ring morphism ? At the end of the code ' hom_map_group_comp' !

import algebra.ring
import tactic
/--
##  It's the group functor  Idem,
##  e1 × e2 = e1 e2 + (1-e1)(1-e2)
-/
structure Idem (R : Type ) [comm_ring R] :=
(e  : R)
(certif :  e * e = e)
namespace  Idem
variables {R : Type }[comm_ring R]                              --   ""
/- extention lemma : E = E' ↔  E.e = E'.e
-/
@[ext]lemma ext : ∀ {g1 g2 : Idem R}, g1.e = g2.e → g1 = g2 := λ g1 g2,
begin
intros h1 ,
cases g1,
cases g2,
congr ; try { assumption },   ---
end
-- We start to define one element : neutral element
def one  : Idem (R) := {e := 1,  certif := mul_one 1}
instance : has_one (Idem R) := ⟨one⟩
-- lemma !
lemma one_e : (1 : Idem(R)).e = 1 := rfl
-- comm ring calculation !
lemma alg_calc (a b : R) : (a * b + (1 - a) * (1 - b)) * (a * b + (1 - a) * (1 - b)) =(a * a) * (b * b) +
((1 - a) * (1 - a)) * ((1 - b) * (1 - b)) + 2* (a* (1 - a)) * (b*(1 - b)) := by ring

lemma compl_e (E : Idem R) : (1-E.e) * (1-E.e)  = (1-E.e)  :=
begin
have H : (1-E.e) * (1-E.e) = 1- 2 * E.e + E.e *E.e,
ring,
rw E.certif at H,
rw H,
ring,
end
/-   e → 1-e
-/
def ortho : Idem R → Idem R := λ E,
begin
exact {e := 1-E.e, certif := compl_e E}
end
lemma ortho_comp (E : Idem R) : (ortho E).e = 1-E.e := rfl
lemma ortho_is_involution (E : Idem R) : ortho (ortho E) = E :=
begin
ext,
rw ortho_comp,
rw ortho_comp,
ring,
end

lemma ortho_e (E : Idem R) : E.e * (1-E.e) = 0 :=
begin
rw [mul_sub_left_distrib,mul_one,E.certif],
exact sub_self E.e,
end
def mul_map' : Idem (R) →  Idem (R) → Idem (R) := λ g1 g2, begin
exact { e := g1.e * g2.e + ((1 : R) -g1.e) * ((1 : R)-g2.e),certif := begin
rw [alg_calc g1.e g2.e,ortho_e g1,g1.certif,g2.certif,mul_zero,zero_mul,add_zero,compl_e g1,compl_e g2], end }
end
instance : inhabited (Idem R) := ⟨1⟩

instance : has_mul (Idem R) := ⟨Idem.mul_map'⟩

lemma e_comp (g1 g2 : Idem R) : (g1 * g2).e = g1.e * g2.e+((1 :R)-g1.e) * ((1 : R)-g2.e) :=  rfl

def mul_inv : Idem R → Idem R := λ g, g

instance : has_inv (Idem R) := ⟨Idem.mul_inv⟩

lemma e_comp_inv (g : Idem R) : (g⁻¹).e =g.e  :=  rfl
meta def Idem_ring : tactic unit :=
[simp only [one_e, e_comp ,e_comp_inv], ring]

run_cmd add_interactive [Idem_ring]

def mul_one'  (g : Idem R) :  g * 1 = g := begin ext; Idem_ring, end
def one_mul' (g : Idem R)  : 1 * g = g := begin ext ;Idem_ring, end
def mul_assoc' (g1 g2 g3 : Idem R) :  (g1 * g2) * g3 = g1 * (g2 * g3) := begin ext; Idem_ring, end

lemma mul_right_inv' (g : Idem R) : g * g⁻¹ = 1 :=
begin
ext,
rw [e_comp,e_comp_inv,g.certif,compl_e,one_e],
simp,
end

lemma mul_left_inv' (g : Idem R) :  g⁻¹ * g = 1 :=
begin
ext,
rw [e_comp,e_comp_inv,g.certif,compl_e,one_e],
simp,
end
instance : group (Idem R) :=
{ mul             := mul_map',
one             := 1,
one_mul         := one_mul',
mul_one         := mul_one',
inv             :=  mul_inv,
mul_assoc       := mul_assoc',
mul_left_inv    := mul_left_inv',}

open is_ring_hom
variables {R' : Type }[comm_ring R'] (f : R →  R')[is_ring_hom f]
def hom_map (f : R →  R')[is_ring_hom f] : Idem (R) → Idem (R') := λ g,
{
e := f g.e,
certif := begin rw [← map_mul (f),g.certif], end
}
lemma e_comp_hom (g : Idem R) : (hom_map (f) (g)).e = f g.e := rfl
meta def Idem_hom : tactic unit :=
[simp only [one_e, e_comp ,e_comp_inv,e_comp_hom,map_add,map_mul], ring]

run_cmd add_interactive [Idem_hom]
lemma hom_map_group_comp  (g1 g2 : Idem R) :
hom_map (f) (g1 * g2) = (hom_map (f) g1) * hom_map (f) g2  := begin
ext,
sorry,   ---------- BRUTAL COMPUTATION ! But i can't !
end

lemma hom_map_one  (g1 g2 : Idem R) : hom_map f (1) = 1 :=
begin
ext,
exact map_one f,
end
end Idem


#### orlando (Mar 26 2020 at 22:36):

ouf ! it's ok ! I just change

meta def idem_hom : tactic unit :=
[simp only [map_add f,map_mul f,map_mul f,map_sub f,map_sub f,map_one f,e_comp_hom,e_comp]]

run_cmd add_interactive [idem_hom]
lemma hom_map_group_comp  (g1 g2 : Idem R) :
hom_map (f) (g1 * g2) = (hom_map (f) g1) * hom_map (f) g2  := begin
ext,
idem_hom,
-- rw [e_comp_hom,e_comp,map_add f,map_mul f,map_mul f,map_sub f,map_sub f,map_one f],
end


#### Kevin Buzzard (Mar 26 2020 at 22:49):

This would be better with bundled ring homs. Then you can just do stuff like rw f.map_mul

#### Kevin Buzzard (Mar 26 2020 at 23:01):

Why mul_one' when it could just be mul_one?

#### Kevin Buzzard (Mar 26 2020 at 23:03):

mul_one and one_mul and mul_right_inv and mul_left_inv could probably all be simp lemmas. In fact I think that you are making some kind of lattice structure, aren't you? Why don't you show that Idem R is a partial order with $a\leq b\iff ab=a$? Is this how it works? Then I think multiplication is some kind of inf operator, and you have a bot and a top.

#### Kevin Buzzard (Mar 26 2020 at 23:04):

In fact I think that you define has_mul on Idem R but I think that this should be has_inf. The symbol for inf is \glb.

#### Kevin Buzzard (Mar 26 2020 at 23:08):

I think you are basically rediscovering some standard lattice structure on the idempotents of a ring. My guess is that you would be better off making an instance of lattice (Idem R) or semilattice_inf_top (Idem R) or whatever it is.

#### Kevin Buzzard (Mar 26 2020 at 23:09):

Then hopefully several of the lemmas you want to prove will already be proved for you because they will be proved for all lattices.

#### Kevin Buzzard (Mar 26 2020 at 23:09):

But you have to use lattice notation ⊓ and not *

#### orlando (Mar 26 2020 at 23:09):

hum interesting !

#### Kevin Buzzard (Mar 26 2020 at 23:10):

It was a big shock to me when Kenny defined a lattice structure on the bundled ideals of a ring and then told me I had to use ≤ when I meant ⊆. But actually now I can see the benefits of using the "correct" lattice notation.

#### orlando (Mar 26 2020 at 23:13):

In fact Idem R, is isomorphic to connected composant of Spec (R), so perhaps, geometricaly, the order is inclusion of component ?

#### orlando (Mar 26 2020 at 23:13):

order i mean the lattice

#### Kevin Buzzard (Mar 26 2020 at 23:14):

Idem R is not just the connected components, it's all the clopen subspaces

Yes true !

#### Kevin Buzzard (Mar 26 2020 at 23:14):

And the order is inclusion yes

#### Kevin Buzzard (Mar 26 2020 at 23:15):

You have to decide whether $ef=e$ will be e<=f or f<=e

#### Kevin Buzzard (Mar 26 2020 at 23:16):

Then one lattice law is just multiplication and the other is 1- then multiply then 1- again

#### Kevin Buzzard (Mar 26 2020 at 23:30):

It sounds like a lattice to me

#### Kevin Buzzard (Mar 28 2020 at 17:16):

@orlando here is the lattice structure.

import algebra.ring
import tactic
import order.bounded_lattice
/--
##  It's the group functor  idem,
##  e1 × e2 = e1 e2 + (1-e1)(1-e2)
-/
structure idem (R : Type ) [comm_ring R] :=
(e : R)
(certif : e * e = e)

namespace idem

variables {R : Type} [comm_ring R]

/-! extension lemma : E = E' ↔  E.e = E'.e -/
@[ext] lemma ext : ∀ {g1 g2 : idem R}, g1.e = g2.e → g1 = g2
| ⟨_, _⟩ ⟨_, _⟩ := λ h, by congr; exact h

-- add a coercion from idem R to R
instance : has_coe (idem R) R := ⟨e⟩

-- Now if E : idem R you can just talk about E : R and this is the same as ↑E : R
-- You don't have to put E.e any more

@[simp] theorem certif_def (E : idem R) : (E : R) * E = E := E.certif

def bot : idem R := {e := 0, certif := mul_zero 0}

instance : has_bot (idem R) := ⟨bot⟩

def inf (E F : idem R) : idem R :=
{ e := E * F,
certif := by rw [(show ((E : R) * F) * (E * F) = E * E * (F * F), by ring), E.certif_def, F.certif_def]
}

-- \glb notation ⊓
instance : has_inf (idem R) := ⟨inf⟩

lemma inf_comm {E F : idem R} : E ⊓ F = F ⊓ E := by ext; apply mul_comm

@[simp] lemma inf_def (E F : idem R) : (↑(E ⊓ F) : R) = E * F := rfl

def le (E F : idem R) := E ⊓ F = E

-- ≤ notation
instance : has_le (idem R) := ⟨le⟩

@[simp] theorem le_def (E F : idem R) : E ≤ F ↔ (E : R) * F = E :=
⟨λ h, begin change E ⊓ F = E at h, show (E ⊓ F).e = E.e, rw h end, @ext _ _ (E ⊓ F) E⟩

instance : partial_order (idem R) :=
{ le := (≤),
le_refl := λ E, begin ext, exact E.certif end,
le_trans := λ E F G hEF hFG, begin
ext,
show (E : R) * G = E,
rw le_def at hEF hFG,
suffices : (E : R) * F * G = E,
{ rwa hEF at this},
rw [mul_assoc, hFG, hEF],
end,
le_antisymm := λ E F hEF hFE, begin
change E ⊓ F = E at hEF,
rw [←hEF, inf_comm],
exact hFE
end }

lemma bot_le {E : idem R} : ⊥ ≤ E :=
begin
ext,
exact zero_mul _,
end

lemma inf_le_left {E F : idem R} : E ⊓ F ≤ E :=
begin
suffices : (E : R) * F * E = E * F,
simpa using this,
rw [mul_comm, ←mul_assoc, E.certif_def],
end

lemma inf_le_right {E F : idem R} : E ⊓ F ≤ F := by rw [inf_comm]; apply inf_le_left

lemma le_inf {E F G : idem R} (hEF : E ≤ F) (hEG : E ≤ G) : E ≤ F ⊓ G :=
begin
suffices : (E : R) * (F * G) = E,
simpa using this,
rw le_def at hEF hEG,
rw [←mul_assoc, hEF, hEG],
end

instance : order_bot (idem R) :=
{ bot_le := λ _, bot_le, ..idem.has_bot, ..idem.partial_order}

instance : semilattice_inf_bot (idem R) :=
{ inf_le_left := λ _ _, inf_le_left,
inf_le_right := λ _ _, inf_le_right,
le_inf := λ _ _ _, le_inf,
..idem.has_inf, ..idem.order_bot
}

-- Should automation generate semilattice_sup_top instance
-- after this definition of inv,
-- and inv_inv and le_of_inv_le_inv?

def inv (E : idem R) : idem R :=
{ e := 1 - E,
certif := begin
rw [(show ((1 : R) - E) * (1 - E) = 1 - 2 * E + E * E, by ring), certif_def],
ring,
end
}

-- ⁻¹ notation for inv
instance : has_inv (idem R) := ⟨inv⟩

@[simp] theorem inv_def (E : idem R) : (↑E⁻¹ : R) = 1 - E := rfl

@[simp] theorem inv_inv (E : idem R) : E⁻¹⁻¹ = E :=
begin
cases E with e he,
ext,
show 1 - (1 - e) = e,
ring,
end

theorem eq_of_inv_eq (E F : idem R) : E⁻¹ = F⁻¹ → E = F :=
begin
intro h,
rw ←inv_inv E,
rw h,
exact inv_inv F
end

theorem le_of_inv_le_inv (E F : idem R) : E⁻¹ ≤ F⁻¹ → F ≤ E :=
begin
intro h,
rw le_def at h ⊢,
have h2 : ((1 : R) - E) * (1 - F) = 1 - E,
simpa using h,
rw [show ((1 : R) - E) * (1 - F) = F * E - (E + F - 1), by ring, sub_eq_iff_eq_add] at h2,
rw h2,
ring
end

theorem inv_le_inv_of_le {E F : idem R} : E ≤ F → F⁻¹ ≤ E⁻¹ :=
begin
intro h,
apply le_of_inv_le_inv,
simp [h],
end

-- I want the next part to be automatically generated
def sup (E F : idem R) := (F⁻¹ ⊓ E⁻¹)⁻¹

-- ⊔ notation (\lub)
instance : has_sup (idem R) := ⟨sup⟩

@[simp] theorem sup_def (E F : idem R) : E ⊔ F = (F⁻¹ ⊓ E⁻¹)⁻¹ := rfl

def top : idem R := ⊥⁻¹

-- ⊤ notation (\top)
instance : has_top (idem R) := ⟨top⟩

@[simp] theorem top_def : (⊤ : idem R) = ⊥⁻¹ := rfl

@[simp] theorem inv_top : (⊤ : idem R)⁻¹ = ⊥ :=
begin
apply eq_of_inv_eq,
simp,
end

theorem le_top {E : idem R} : E ≤ ⊤ :=
begin
apply le_of_inv_le_inv,
convert bot_le,
simp,
end

instance : order_top (idem R) :=
{ le_top := λ _, le_top, ..idem.has_top, ..idem.partial_order}

-- a machine could write these
instance: semilattice_sup_top (idem R) :=
{ le_sup_left := λ E F, begin
apply le_of_inv_le_inv,
rw sup_def,
rw inv_inv,
apply inf_le_right,
end,
le_sup_right := λ E F, begin
apply le_of_inv_le_inv,
rw sup_def,
rw inv_inv,
apply inf_le_left,
end,
sup_le := λ E F G hEF hFG, begin
apply le_of_inv_le_inv,
rw sup_def,
rw inv_inv,
apply le_inf (inv_le_inv_of_le hFG) (inv_le_inv_of_le hEF),
end,
..idem.has_sup, ..idem.order_top
}

instance : bounded_lattice (idem R) :=
{
..idem.semilattice_inf_bot, ..idem.semilattice_sup_top
}


#### orlando (Mar 28 2020 at 17:22):

ohhh thx kevin !!!

#### Kevin Buzzard (Mar 28 2020 at 17:22):

I think that this bounded lattice structure is somehow the fundamental structure on idem. I believe that you can make it into a ring as well -- you just made it a group I think.

#### orlando (Mar 28 2020 at 17:24):

hum i don't know if there is a natural ring structure !

#### Kevin Buzzard (Mar 28 2020 at 17:29):

Lenstra told me about it in 1996 :-) it's a Boolean ring IIRC

#### orlando (Mar 28 2020 at 17:45):

I try to explain a little the maths ! (in english it's difficult :sweat_smile:) !

I use idempotent, for " sheafifying " finite constant group (for Zariski topology). Here it's just a little example, the good objet is the functor of complete indempotent orthogonal familly i.e ( $(e_i)_{ i \in \{ 1,\dots,n\}}$ s.t $\sum e_i = 1$ and $e_i e_j =0$ and $e_i^2 = e_i$ !

Little exemple with $\text{Idem}$ and the finite constant group generate by the matrix $\begin{bmatrix} 0 & 1\\ 1 & 0 \end{bmatrix}$ !

I make $2$ objet (= functor),

$B: R \mapsto \{ (a,b) \in R^2 \mid a^2-4b \text{ invertible} \}$

And

$X : R \mapsto \{ (x,y) \in R^2 \mid (x-y)^2 \text{ invertible} \}$

You have a map $\pi : X \to B$ given by $(x,y) \mapsto (x+y,xy)$.

The fact is that $\text{Idem}(R)$ act on $X$ over $B$, the action is given by

$e \star \begin{bmatrix} a \\ b \end{bmatrix} := \begin{bmatrix} e & 1-e\\ 1-e & e \end{bmatrix} \begin{bmatrix} a \\ b \end{bmatrix}$

For exemple if $e=0$ the action is $(a,b) \mapsto (b,a)$ ! (classical one, the system is symmetric) !

And all this stuff are functorial !

The fact is that the action is " simply transitive " (i thinck it's the official terminology) i.e transitive without fixed point ! So the group act simply transitive on fiber like topological cover !

As an example :

sage: R
Ring of integers modulo 2457
sage: G = lambda e : M([R(e),R(1-e),R(1-e),R(e)])  # M
sage: idem
[0, 1, 351, 378, 729, 1729, 2080, 2107]
sage: R(a)
409
sage: R(b)
2268
sage: S                              #### couple solution x+y = a   &  x*y = b
[[189, 220],
[220, 189],
[675, 2191],
[787, 2079],
[1242, 1624],
[1624, 1242],
[2079, 787],
[2191, 675]]
sage: v                           #### a particular solution
(220, 189)
sage: [G(e)*v for e in idem]   ####  orbit of v for  Idem action  ---> all the solution !!!
[(189, 220),
(220, 189),
(1242, 1624),
(2079, 787),
(675, 2191),
(2191, 675),
(787, 2079),
(1624, 1242)]


#### orlando (Mar 28 2020 at 17:48):

Thanks for the ring structure, I'm going to meditate on it to see if there is anything interesting to say !

#### orlando (Mar 28 2020 at 18:28):

coersion is good !!!

#### Kevin Buzzard (Mar 28 2020 at 18:53):

If you think about the elements as clopen sets, then addition is symmetric difference and multiplication is intersection.

#### Kevin Buzzard (Mar 28 2020 at 18:54):

After I add the coercion, I am careful to never mention .e again. I only talk about (E : R) or \u E, and I train all my simp lemmas using the coercion notation.

#### Kevin Buzzard (Mar 28 2020 at 20:42):

The coercion is the "canonical notation" for the confluent rewriting thingamajig that we are trying to set up with simp

#### Kevin Buzzard (Mar 28 2020 at 20:42):

Darn it, I am one buzzword short

#### orlando (Mar 29 2020 at 07:27):

@Kevin Buzzard : For the structure of ring. I'am not good with the prime spectrum and topology but : $\text{Idem}(R)$ "is equivalent" to locally constant fonction $\text{Spec} (R) \to \{ 0,1\}$ and on $\{0,1\}$ there is ring structure.

For the lattice, i don't really use this kind of structure (in maths) ! So i will take some time !

#### Kevin Buzzard (Mar 29 2020 at 09:17):

Lattice: it is not difficult. It's just a partial order with sup and inf and some axioms. inf is the min of two things, id is the min of one thing, top is the min of 0 things, so now by induction we can take the minimum of any finite set. Same for max

#### Kevin Buzzard (Mar 29 2020 at 09:18):

Functions to {0,1}: yes that's what's going on

Last updated: Dec 20 2023 at 11:08 UTC