Group morphism

Stream: general

[orlando]

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]

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]

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

[Kevin Buzzard]

Why mul_one' when it could just be mul_one?

[Kevin Buzzard]

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]

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]

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]

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]

But you have to use lattice notation ⊓ and not *

[orlando]

hum interesting !

[Kevin Buzzard]

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]

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

[orlando]

order i mean the lattice

[Kevin Buzzard]

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

[orlando]

Yes true !

[Kevin Buzzard]

And the order is inclusion yes

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

It sounds like a lattice to me

[Kevin Buzzard]

@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]

ohhh thx kevin !!!

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[orlando]

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]

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

[orlando]

coersion is good !!!

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Darn it, I am one buzzword short

[orlando]

@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]

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]

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