Petros Mavromichalis

Stream: new members

[Petros Mavromichalis]

Hello everyone,
I'm Petros, I am an undergrad at California State University Northridge, and I have been working with my abstract algebra professor this past semester to understand... well to understand what's up with lean!

I just learned the Isomorphism Theorems for groups, rings, and modules recently so I've been trying to understand where (if) these theorems are in matlib.
I started with the natural number game and the tutorials, and I've read through the reference manual and I've dug around the documentation for matlib (and I went on quite an adventure learning how lean handles quotients) and eventually I found the documentation of the isomorphism theorems for setoids and monoids.

And now I'm not sure how to proceed!

I booted up lean in VScode with the hope of coding up the third isomorphism for rings myself, but I got stuck trying to define a group homomorphism from one quotient group to another.

[Adam Topaz]

One place you could look is here
https://leanprover-community.github.io/mathlib-overview.html

[Adam Topaz]

For example the first iso thm for groups appears under group theory there.

[Kevin Buzzard]

All this stuff is possible in Lean. Why not post a #mwe showing how far you've got? The two main tools to define maps from quotient groups are in group_theory.quotient_group and they're quotient_group.lift and quotient_group.map.

[Kevin Buzzard]

Mathematically, quotient_group.lift gives you a group homomorphism $G/N\to H$ from a group homomorphism $G\to H$ with $N$ in the kernel, and quotient_group.map gives you a group homomorphism $G/N\to H/M$ from a group homomorphism $G\to H$ which sends $N$ into $M$. I'm reluctant to say too much more without a #mwe though to check we're on the same page.

[Petros Mavromichalis]

Yes thank you! I did know the first isomorphism theorem was there, but I haven't seen as much on the third.

[Petros Mavromichalis]

I'm not savvy on how to include code in my post

[Kevin Buzzard]

You might find it stated in a surprising way here, for example one could say that the lattice of subgroups of G containing N was order-isomorphic to the lattice of subgroups of G/N. This could be naturally expressed in Lean but it might not be the way to explain it to an undergraduate.

[Kevin Buzzard]

Code in post: put ``` on a line by itself at the beginning, then code under it, and then ``` on a line by itself at the end. Make sure you include all imports etc etc.

[Petros Mavromichalis]

import ring_theory.ideal.basic

variables (R: Type*)

def third_iso_theorem_rings (r : R) (I J : ideal R) (A : I ≤ J) (f : I.quotient → J.quotient) (h : f(I.quotient.mk r) = (J.quotient.mk r)):
 quotient(ker(f) I.quotient) ≃ J.quotient :=
begin
  sorry
end

Definitely not a working example, this is the structure of what I want and I have been correcting it piece by piece

[Kevin Buzzard]

Yeah this is not working at all :-) The first error is that Lean complains that it doesn't know that R is a commutative ring, so you'd better add [comm_ring R] to your list of variables to make R a commutative ring, assuming you want to prove a theorem about commutative rings (this is exactly why mwes are important, so we can establish what you think the theorem is).

[Petros Mavromichalis]

oops! yes it definitely isn't going to work even with that fix haha
I'm trying to wrap my head around how I.quotinet.mk works at the moment, because that is the next failure point

[Kevin Buzzard]

Yeah, I honestly don't understand why projection notation isn't working there. You can fix it with (h : f(ideal.quotient.mk I r) = (ideal.quotient.mk J r)).

[Kevin Buzzard]

Right now your definition says that if I and J are ideals of R and if r is an element of R, and if you have a random function from $R/I$ to $R/J$ which sends $r+I$ to $r+J$ then...something. What mathematically do you want to conclude?

[Kevin Buzzard]

PS I am about to go to bed (I'm in UK) so I'll have to leave you to someone else. Another issue presumably is that right now $f$ is just a set-theoretic function, which is probably not what you want, and your hypothesis involves some random element $r$ of the ring, which presumably isn't what you want either (for example $r$ could be 0 and then if $f$ is a ring homomorphism then $h$ will be automatic).

[Kevin Buzzard]

This will be the reason you're getting nowhere with ker(f) -- a random map between two types (or sets or however you want to think about them) doesn't have a kernel, you're going to need more structure on f before the concept of a kernel makes sense.

[Petros Mavromichalis]

Okay, thank you very much!
Would a quantifier fix that right away?
(h : ∀ r : R, f(ideal.quotient.mk I r) = ideal.quotient.mk J r)

[Kevin Buzzard]

Well I don't know what you're trying to say mathematically yet, but that looks like a more useful statement than what you have right now.

[Kevin Buzzard]

Aah, you want to say that $(R/I)/(\mathrm{ker}(f))$ is isomorphic to $R/J$?

[Kevin Buzzard]

Right now you're claiming that you an construct a bijection of sets (or strictly speaking of types, because we're doing type theory, but a type is the same as a set in this context)

[Petros Mavromichalis]

right this is where I am at now,

import ring_theory.ideal.basic

variables (R: Type*) [comm_ring R]

/-The third isomorphism theorem for rings outline:
  For ideals I J of ring R
  with I ≤ J as addative groups
  If
  ∀ r ∈ R
  f: R/I → R/J
  f(r + I) = r + J

  then
  f is a group homomorphism with
  ker(f) = J/I and
  (R/I)/ker(f) ≃ R/J
-/

def third_iso_theorem_rings (I J : ideal R) (A : I ≤ J)
(f : I.quotient → J.quotient) (h : ∀ r : R, f(ideal.quotient.mk I r) = (ideal.quotient.mk J r)):
 quotient(ker(f) I.quotient) ≃ J.quotient :=
begin
  sorry
end

[Kevin Buzzard]

You are claiming a lot of stuff in your comment. This looks more like three lemmas than one.

[Kevin Buzzard]

If you don't want to assume that f is a ring homomorphism or a group homomorphism then you'll have to prove that first, before you can even talk about the kernel of f.

[Kevin Buzzard]

import ring_theory.ideal.basic

variables (R: Type*) [comm_ring R]

lemma f.map_add (I J : ideal R) (A : I ≤ J) (f : I.quotient → J.quotient)
  (h : ∀ r : R, f(ideal.quotient.mk I r) = ideal.quotient.mk J r) :
∀ a b : I.quotient, f (a + b) = f a + f b :=
begin
  sorry
end

might be a place to start.

[Kevin Buzzard]

But this is quite tricky! You will need to be a master of lean quotients to figure out how to do this.

[Kevin Buzzard]

Do you know the maths proof?

[Kevin Buzzard]

docs#ideal.quotient

[Petros Mavromichalis]

Okay, I have a lot more work to do then! I think I know where to take this from here :)
I do know the proof

[Eric Wieser]

(answering an earlier point - projection notation allows f.bar to mean foo.bar f for f : foo, but you can't chain multiple dots together and expect f.bar.baz to mean foo.bar.baz f)

[Kevin Buzzard]

Hmm, I can't see the inductive principle you need, you might have to get your hands dirty with docs#ideal.quotient.mk_surjective . Good luck! I'll be back in about 8 hours :-)