Zulip Chat Archive

Stream: new members

Topic: Petros Mavromichalis


Petros Mavromichalis (Apr 09 2021 at 22:13):

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 (Apr 09 2021 at 22:17):

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

Adam Topaz (Apr 09 2021 at 22:17):

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

Kevin Buzzard (Apr 09 2021 at 22:18):

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 (Apr 09 2021 at 22:20):

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

Petros Mavromichalis (Apr 09 2021 at 22:24):

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

Petros Mavromichalis (Apr 09 2021 at 22:25):

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

Kevin Buzzard (Apr 09 2021 at 22:25):

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 (Apr 09 2021 at 22:26):

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 (Apr 09 2021 at 22:29):

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 (Apr 09 2021 at 22:32):

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 (Apr 09 2021 at 22:35):

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 (Apr 09 2021 at 22:36):

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 (Apr 09 2021 at 22:38):

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/IR/I to R/JR/J which sends r+Ir+I to r+Jr+J then...something. What mathematically do you want to conclude?

Kevin Buzzard (Apr 09 2021 at 22:40):

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 ff is just a set-theoretic function, which is probably not what you want, and your hypothesis involves some random element rr of the ring, which presumably isn't what you want either (for example rr could be 0 and then if ff is a ring homomorphism then hh will be automatic).

Kevin Buzzard (Apr 09 2021 at 22:40):

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 (Apr 09 2021 at 22:45):

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 (Apr 09 2021 at 22:46):

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 (Apr 09 2021 at 22:47):

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

Kevin Buzzard (Apr 09 2021 at 22:48):

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 (Apr 09 2021 at 22:49):

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 (Apr 09 2021 at 22:50):

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

Kevin Buzzard (Apr 09 2021 at 22:50):

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 (Apr 09 2021 at 22:52):

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 (Apr 09 2021 at 22:56):

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

Kevin Buzzard (Apr 09 2021 at 22:56):

Do you know the maths proof?

Kevin Buzzard (Apr 09 2021 at 22:58):

docs#ideal.quotient

Petros Mavromichalis (Apr 09 2021 at 22:58):

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 (Apr 09 2021 at 22:59):

(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 (Apr 09 2021 at 23:02):

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 :-)


Last updated: Dec 20 2023 at 11:08 UTC