--- layout: archive title: Zulip Chat Archive permalink: /stream/113488-general/topic/statement.20of.20the.20five.20lemma.html ---
I just wrote a statement of the five lemma: https://gist.github.com/jcommelin/d097eb8f2587d34e5c337450bca543db
It seems extremely verbose to me. (And no, removing line breaks is not the solution :wink: ...)
If we ignore the facts that I am (i) not using lowercase greek for types, (ii) write types and conditions in the wrong order, and (iii) write lots of linebreaks; are there ways to improve this statement?
Not nearly as verbose as the proof, I'm sure :simple_smile:
One thing you could do is package up the underlying set function and is_group_hom
instance of each map into a single type
I would love to just say: "Hey Lean, all these types are groups, and by the way, all my functions are homomorphisms"
sancta mater dei
you formalized five lemma
@Kevin Buzzard this is dank
no I did not
Only the statement
that’s what i mean
Which is not so hard to formalise, right?
formalize [sth] = formalize the statement of sth
well I never got my hands dirty
It's just a lot of repetitive strain injury inducing introductory blabla typing
I'm scared of the proof atm
But I hope that cc
will do a lot of diagram chasing for me
Currently my proof starts with split, apply is_group_hom.inj_of_trivial_ker n
. And then I'm stuck, because I don't know how to prove that two subsets are equal...
I really need a lot of handholding with Lean :confounded:
How do you split the goal subset_1 = subset_2
into proving x \in subset_1 \to x \in subset_2
and its converse?
You can apply set.ext
(I was just about to write something longer, but you said just what it does.)
Thanks, that helps. Now I get an \iff
. How do I split it into two implications?
(And more meta: what is the best way to discover the answer to these questions without spamming Zulip?)
Either you use iff.intro
or the anonymous constructor written as \< ... , ... \>
where the VS Code plugin replaces the \<
and \>
.
Ok, cool
thanks!
Alternatively: use subset.antisymm
then you have it in the right form (the subset relation is defintional equal to forall x subset_1 implies subset2
What are the advantages of subset.antisymm
over the other method?
@Johan Commelin use split
to break down an iff
In this specific case, I imagine there's probably a lemma that says that it suffices to show that f x = 0 \to x = 0
Yeah, I've got the trivial part now. If x \in trivial subgroup \to x \in ker
that's paraphrasing
Can I easily rewrite the hypothesis (com₁ : m ∘ f = r ∘ l)
into com₁' : \fo x, (m (f x) = r (l x))
?
Here's my attempt to syntactically follow the lemma.
It probably won't help you prove anything, of course. :simple_smile:
I mean, shouldn’t one prove the weak four lemmas first?
One could, of course... but they are basically the two subgoals after the first split
There is a good reason to do that though... because then you only have to prove one of them
the other follows by duality
Still, the proof is a very straightforward diagram chase... so I hope I can convince Lean that it is easy as well
I want to tell lean "For every group_hom \phi that you can see, do this... have := is_group_hom.one \phi
"
And things like that
And one it has figured out all these basic things, then cc
might actually deduce the result
But then cc
needs to know how to deal with \circ
, hence my previous question about rewriting com\1
@Sean Leather Thanks for the refactoring. It is more readable now (except that I most I would give the arrows names like f_1, g_1 and f_2, g_2 etc...)
But it is still a bit verbose, right?
I added a comment with an "artistic" layout
(warning: long lines)
Ha! I like that one
It really explains the diagram. Cool!
It would be great of you could tell lean [is_group_hom f g h i j k l]
something like that, and it just understands that all of them are group homs
It would be great of you could tell lean
[is_group_hom f g h i j k l]
Something like that would be useful in your case, but you wouldn't want to remove the ability to use multiple-parameter type classes, which it looks like is_group_hom
is there.
Hmmz, I see
Also: ↪
and ↠
for injective respectively surjective functions
But I guess that might be a bit hard
So {f: A ↪ B}
means {f: A → B} [function.injective f]
At the very least, you can open function
to avoid having to prepend function.
. :simple_smile:
Aaah, ok. TIL :)
Hmmz TIL is confusing in this context. I meant "Today I Learned"
(And more meta: what is the best way to discover the answer to these questions without spamming Zulip?)
Spam Zulip. I was in just this situation last September and spamming Zulip was by far the most efficient method. Mario often answered very quickly, and several others too. Now there are more people who can help, and the sooner you're up to speed the sooner you can help others. It's really important that mathematicians learn how to use this software as quickly as possible.
PS I hope you're going to implement the abstract abelian category proof rather than all the diagram-chasing ;-)
[not serious]
although, in this crazy, world, who's to say that the abstract universal property proof won't be easier!
I find myself in a similar situation right now, as it happens.
I would like to prove R[1/f][1/g] = R[1/fg] (unique isomorphism of R-algebras)
and I have set up all these universal properties and I know I can deduce it from those, and it will be really nice to do
but I suspect that if I were to ask Kenny he would just write down a proof with lots of quotient.mk's in which just did everything directly.
i.e. we have an interface (i.e. a bunch of universal properties) which will enable me to prove my result, but now I realise that someone who knows the underlying implementation can just prove the result directly anyway.
It might be the same here; you can deduce the 5 lemma from the axioms of an ab cat
or from the diagram chase
and the proofs will be very different
Yes, I see. I think it should be possible to have a diagram_chase tactic
And my gut feeling is that cc
is almost it. But you need to spam the context with a lot of information about group homomorphisms and kernels etc...
diagram_chase
tactic: I wonder if that's possible!
As far as I know these CS people don't really do this kind of maths
so you might find that this is actually a possibility once you formalise what you want
That would be sooo nice
When drawing that snake map from ker(map3) to coker(map1) I always feel I'm making the unique move each time
Is the new parser going to accept tikz-cd
input?
As far as I know these CS people don't really do this kind of maths
:astonished: Diagrams are pretty core to PLT.
PLT?
diagram-chasing in abelian groups is perhaps a bit different
Programming language theory.
thks
diagram-chasing in abelian groups is perhaps a bit different
Okay. I'm not familiar with it, so that may be.
Is the theory of abelian categories "complete" in some way?
Yes, I was thinking about tikz-cd as well (-;
i.e. "the five lemma is true, so there should be a proof which an algorithm can construct"?
Just think, we could pester Mario to spend weeks developing such an algorithm, and then use it to prove the five lemma and then say "actually, the five lemma is pretty much the only thing we ever use"
@Patrick Massot Did you see how @Reid Barton rewrote the statement? https://gist.github.com/jcommelin/d097eb8f2587d34e5c337450bca543db
"but thanks anyway"
Ouch
And the snake lemma, and the rest of homological algebra
That PR will be rejected because the groups aren't all called alpha
Yeah, I will relabel everything to be alpha_1 alpha_2 etc...
who needs betas
I concur with Kenny's "dank" comment
This is absolutely great
No, you should keep groups G. Mario and Johannes will end up understanding.
Don't release pressure on this important issue
Sure
Was just kidding
@Kevin Buzzard Well, thanks. I thought it was a good test case
Is the theory of abelian categories "complete" in some way?
No, https://mathoverflow.net/a/12799
Most similar theories will admit embeddings of the word problem like this, I think. But in diagrams where there are only finitely many ways to compose morphisms (basically, "without loops"), maybe there is hope.
Thanks @Reid Barton . I wondered if the abelian-ness of the situation saved our bacon but somehow this automorphism trick gets you back into a non-abelian situation
I put an update in the comments of the gist: https://gist.github.com/jcommelin/d097eb8f2587d34e5c337450bca543db
The first half of the proof is almost done
There is one stupid admit
And I don't get why apply_assumption
fails, because 2 lines above, there is f_1 w = y
Your definition of im is not great
You defined definition im (f : A → B) [is_group_hom f] := f '' (@set.univ A)
No, no longer
See the update
Oh OK
It is now set.range f
I dunno if that is better (-;
That's definitely better
The problem with the old one
definition im (f : A → B) [is_group_hom f] := f '' (@set.univ A)
was that you can write #print notation ''
to find out what ''
expands to
and see it expands to set.image
and then #print set.image
to find what that unfolds to
I see...
and you see it becomes \ex a, a \in set.univ and f a = b
in particular we have some clause which is always true
and in the way
With your new definition we can do stuff like this:
import group_theory.subgroup open function is_group_hom universes u variables {A B : Type u} [group A] [group B] definition im (f : A → B) := set.range f example (G H K : Type u) [group G] [group H] [group K] (α : G → H) [is_group_hom α] (β : H → K) [is_group_hom β] (Hexact : im α = ker β) (h : H) (Hker : β h = 1) : ∃ g, α g = h := begin have Hker2 : h ∈ ker β := (mem_ker β).2 Hker, rw ←Hexact at Hker2, exact Hker2 end
because after the rewrite, Hker2
is definitionally equivalent to what you want
I still think you should prove the weak four lemmas first
@Kenny Lau I am almost done with the first one
Just need to get rid of one stupid admit
It's really hard to follow the argument without working hard
what is the problem which you're admitting defeat on?
I see you want to prove y in im f1
and I see 100 assumptions
Ok, so a minor change. I now have local notation im := set.range
with backticks around im
if you open set you can just use range
but I think im is better
what is your maths proof of the thing you;re admitting?
So, I want to prove y ∈ im f
and it should follow immediately from the two lines above it
I see
so name one of them and use rw?
Although I am not an expert
aha, I thought apply_assumption would just kill it off
I am skeptical about not naming any assumptions
I have never heard of apply_assumption
What does it do?
It is like apply foo
, where foo
is an assumption
but you need 2 assumptions
to deduce what you want
yeah, that's true
I don't think it's the end of the world to start calling useful hypotheses H1 H2 H3...
But rw
doesn't work either... I named one of the assumptions:
have foo : f₁ w = y
And then I try rw foo
, but it doesn't work
rw \l foo
unknown identifier 'foo'
I think that you are not proving what you think you are proving
have foo : f₁ w = y, apply_assumption,
That's what you have now, right?
Yes
so put your cursor just after the comma after the y
and you see that the first goal is f1 w = y
and there are two goals
Yes
and now click after the comma after apply_assumption
and there are still 2 goals
aaah
so your "proof" didn't prove it
this is nothing to do with the naming of the assumption
it was just never added to the local context
ok, thanks!
let me try again
Because your context is gigantic
you should keep a close eye on the number of goals
which is displayed at the top of the output
{% endraw %}Last updated: Apr 24 2020 at 19:02 UTC


Table of Contents
Intro
Hello dear friend(s)!
Welcome!
I started this to share some of my little nuggets of learning on the way to Haskell heaven--sort of like a local travel-guide, recommending the best eateries, tea shops, etc.
Needless to say, there are tons of various pieces of useful info about Haskell, its awesome features, community & eco-system on the internet. (Check out the References page if you want that.)
But what I have seen to be lacking among students intending to learn Functional Programming with or without Haskell is a deeper appreciation & understanding of the core concepts on top of which the whole realm of Functional Programming (of which Haskell is a torch-bearer!) is built, namely the concept of functions, types, and how they are beautifully represented by Haskell in their purest forms. Knowing these concepts properly leads one to experience Aha! moments and such sheer joy! After all, our lives should be filled with such Joys & Thrills of discovery!
To reiterate, this series of articles is NOT a set of Haskell Tutorials. Interested readers can consult the References page for pointers regarding these. What I want to do here is try & share the subtle patterns & beauty in Haskell in particular, especially highlighting how they reflect the core mathematical ideas. If these "essays" could stoke the fire in you & your friends to plunge into the Pilgrimage to Haskell Heaven, I would be so happy indeed! And I'm sure that any such traveller will be rewarded with unforgettable "views" along the way!
Happy Journey! And Let's Get Started !!!


This is a wider card with supporting text below as a natural lead-in to additional content. This content is a little bit longer.
Last updated 2 years ago
This is a wider card with supporting text below as a natural lead-in to additional content. This content is a little bit longer.
Last updated 1 year ago
This is a wider card with supporting text below as a natural lead-in to additional content. This content is a little bit longer.
Last updated 2 years ago
This is a wider card with supporting text below as a natural lead-in to additional content. This content is a little bit longer.
Last updated 1 year ago
This is a wider card with supporting text below as a natural lead-in to additional content. This content is a little bit longer.
Last updated 2 years ago
This is a wider card with supporting text below as a natural lead-in to additional content. This content is a little bit longer.
Last updated 1 year ago
This is a wider card with supporting text below as a natural lead-in to additional content. This content is a little bit longer.
Last updated 2 years ago
This is a wider card with supporting text below as a natural lead-in to additional content. This content is a little bit longer.
Last updated 1 year ago
This is a wider card with supporting text below as a natural lead-in to additional content. This content is a little bit longer.
Last updated 2 years ago
This is a wider card with supporting text below as a natural lead-in to additional content. This content is a little bit longer.
Last updated 1 year ago
This is a wider card with supporting text below as a natural lead-in to additional content. This content is a little bit longer.
Last updated 2 years ago
This is a wider card with supporting text below as a natural lead-in to additional content. This content is a little bit longer.
Last updated 1 year ago
This is a wider card with supporting text below as a natural lead-in to additional content. This content is a little bit longer.
Last updated 2 years ago
This is a wider card with supporting text below as a natural lead-in to additional content. This content is a little bit longer.
Last updated 1 year ago
This is a wider card with supporting text below as a natural lead-in to additional content. This content is a little bit longer. Lorem ipsum dolor, sit amet consectetur adipisicing elit. Vitae voluptates, non voluptas iusto natus voluptate facilis eos sequi dignissimos dolores?
Lorem ipsum dolor sit amet consectetur adipisicing elit. Dolor totam veritatis libero corrupti quos architecto ab eos consequuntur eaque, quibusdam eveniet minima adipisci, cupiditate voluptatum? Incidunt veritatis quia et ab!
Lorem ipsum dolor sit amet, consectetur adipisicing elit. Labore molestias cum itaque deserunt velit nemo voluptatem unde sequi repellat ratione ipsa, quo explicabo accusamus dolores officiis aliquid non!
Lorem ipsum dolor sit amet consectetur adipisicing elit. Nostrum blanditiis modi eos quia recusandae ullam aliquam sequi cumque suscipit nam velit, hic unde quis odio similique!
Last updated 3 mins ago


Clear Data | Display Data Add a NewHire Add A New Hire * Fields are required First Name:* Last Name:* Hire Date: Active: Position:* Experience: Windows XP Windows 7 Swipe ID:* Phone Extension:* Notes: test Add New-Hire


AngularJS CRUD
Features
Enterprise
Support
Pricing
Github
Name required!
Email required!
Password required!
Add
Update
Details
Name
Email
Password
Actions
{{item.name}}
{{item.email}}
{{item.password}}


First Elder Lockirin:
The First Elder cannot give Recommendations. This is one way his powers are restricted. You must receive Recommendations from the other 3 Elders.


{% extends "base.html" %} {% set active_page = "login" %} {% from "security/_macros.html" import render_field_with_errors, render_field, render_field_errors %} {% from 'global/macros/login_form_macros.html' import email with context %} {% from 'global/macros/login_form_macros.html' import password with context %} {% from 'global/macros/login_form_macros.html' import text with context %} {% from 'global/macros/form_macros.html' import checkbox with context %} {% from 'global/macros/form_macros.html' import checkbox_checked with context %} {% block content %}


--- title: Fran Berger date: 2017-01-10 00:00:00 Z layout: project type: project subtitle: Web Development background: "/img/projects/fran-berger/fran-thumb.png" ---
Fran Berger is an entrepreneur, lifestyle and home entertaining expert and a restaurateur. As a frequent media contributor, Fran shares and educates about the many creative ways that we can build and strengthen relationships while gracefully entertaining at home; the way we encourage interpersonal and intimate connections among those around us at mealtime.


Backend hacker, Ruby and iOS/Mac developer. Co-Founder and Software Astronaut at Mocha Industries. Awesome skier. Future American. Homepage


--- layout: page permalink: /publications.html title: Publications header-img: last-updated: 2020-10-30 5:55 PM --- {% assign theme = site.data.themes[site.ui_theme] %}


Detached House
.
5Y OLD
$750,000
742 Evergreen Terrace
3
Bedrooms
3
Bedrooms
Owner
Tiffany Heffner
(516) 996-254


Surrounding scope:{{myProperty}}
Inside an directive with inherited scope:{{myProperty}}
in side myDirective, isolate scope:{{myProperty}}


This page allows you to trigger the re-indexing of the site.
Click here to re-index every node on the site
Re-Indexing Triggered.
Click here to delete the index and re-create from scratch. This can be useful if you're having problems.
Index Re-Creation Triggered.


I experimented with Sage Goddess Emerald Essence on three occassions in 2003. This is a report of my experiences on those three occassions. To give you some background, I have practised various meditation techniques since 1990, and have had the occassional interesting and 'meaningful' dream experiences and 'visions' which I attribute to particularly successful meditation sessions. I am attracted to the philosophies of Advaita, Buddhism and Zen, which describe the phenomenal universe and the sense of self as illusory, with Awareness being the sole underlying reality. I really do not have much of a record of experimenting with drugs, hallucinogens or entheogens, except for using pot sporadically, and a sole LSD experience on top of a hill in the forests that was entertaining, but not particularly coherent or meaningful. In other words, all my so-called 'meaningful' experiences have been either spontaneous or meditation-induced, not substance-induced.
Salvia Experience #1 (sometime in 2003):
I was on the floor of my bedroom at night. I squirted a couple of dropperfuls of Emerald Essence into my mouth and held the stinging, bitter liquid in my mouth for about 20 minutes. I spat the liquid out, and feeling very, very sleepy, drifted off to sleep. Something was conscious of a very loud, deep bass thumping sound, and an enveloping darkness. I say 'something', because I was not aware of myself as a human or an embodied, self-aware being, in some sense, I was the sound. But yet paradoxically, 'I' was aware of the sound. The sound was extremely loud and I could not figure out what it was, nor was I making any attempt to discern its cause. Why would I? I was just aware, with no motive. I could hear every nuance in this sound.
Slowly, awareness of self returned. The source of the sound suddenly dawned upon me, it was my heart beating. I was now aware of myself as a tiny point somewhere deep inside my body, in total darkness (my eyes were closed), and I could hear my heart beating deeply, loudly, as if it were filling a cathedral.  In retrospect, the experience did not feel like a hallucination at all. Instead, it felt like a genuine, hyper-sensory experience.
Salvia Experience #2 (sometime in 2003):
I was in the same setting as in the previous experience, on the floor of my bedroom. After holding the Emerald Essence in my mouth for about 20 minutes, I spat the liquid out, and again, feeling very, very sleepy, drifted off to sleep. This time, 'I' was conscious of a very loud, rushing sound, and an enveloping darkness. Again, the sound was extremely loud and all encompassing, and as before, you could say that I was the sound. I could hear every nuance in this sound. When my awareness of self returned, the source of the sound suddenly dawned upon me, it was my breathing.
I was now aware of myself as a tiny point somewhere deep inside my body, in total darkness. My body was still asleep and breathing restfully. I could hear every nuance in the sound of my breathing with a heightened perception. Think of being in a giant wind tunnel and hearing the wind rush by.  Again, the experience felt like a genuine, hyper-sensory experience.
Salvia Experience #3 (sometime in 2003):
On this occassion, I was alone at home in the daytime. If I recall right, I took a larger dose than on the previous two occassions. After holding the Emerald Essence in my mouth for about 20-30 minutes, I lay down with my eyes closed. Soon, I started seeing visuals, strange geometric patterns and colors that I perceived to be 'trivial' and mildly annoying. At some point, my sense of self dissolved completely. I suddenly felt I had become a set of buildings, roads and vehicles in the neighborhood I grew up in as a teenager.
I was not a human or organic being anymore, I was a set of insentient objects. There was simply no memory of my past existence as a person. What's more, I wasn't one, I was many. This was the weirdest sensation of them all. We are normally used to being or identifying with one thing or self, not a multiplicity of things at the same time. While the imagery associated with this feeling was a typical hallucination, the experience of being many things at once is apparently within the capacity of the mind, otherwise I could not have experienced it.
Experience Reports are the writings and opinions of the individual authors who submit them.
Some of the activities described are dangerous and/or illegal and none are recommended by Erowid.