feat(group_theory/congruence): quotients of monoids by congruence relations #1710
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
jcommelin
approved these changes
Nov 19, 2019
src/group_theory/congruence.lean
Outdated
| defined by '`x ≈ y` iff the elements of `f⁻¹(x)` are related to the elements of `f⁻¹(y)` | ||
| by `c`.' -/ | ||
| @[to_additive "Given an addition-preserving function `f` whose kernel is contained in an additive congruence relation `c`, the smallest additive congruence relation containing the binary relation on `f`'s image defined by '`x ≈ y` iff the elements of `f⁻¹(x)` are related to the elements of `f⁻¹(y)` by `c`.'"] | ||
| def map_gen (f : M → N) (H : ∀ x y, f (x * y) = f x * f y) (h : mul_ker f H ≤ c) : con N := |
There was a problem hiding this comment.
You never use h or H here.
Is there some mad result here, like if I quotient N by this relation, then f \comp quotient.mk is multiplicative even if f isn't?
There was a problem hiding this comment.
Just thought about it and there isn't any result like that.
src/group_theory/congruence.lean
Outdated
| the quotient induces a congruence relation on `f`'s domain defined by '`x ≈ y` iff `f(x)` is | ||
| related to `f(y)` by `d`.' -/ | ||
| @[to_additive "Given an additive congruence relation `c` on a type `M` with an addition and an addition-preserving map `f` to the quotient of `M` by `c`, an additive congruence relation `d` on the quotient induces an additive congruence relation on `f`'s domain defined by '`x ≈ y` iff `f(x)` is related to `f(y)` by `d`.'"] | ||
| def comap (f : N → c.quotient) (H : ∀ x y, f (x * y) = f x * f y) |
There was a problem hiding this comment.
There's no need for the image of f to be a quotient of N here I don't think.
There was a problem hiding this comment.
Thank you, damn, I see I didn't properly address this in setoid.lean when you mentioned it either.
src/group_theory/congruence.lean
Outdated
| /-- Restriction of a congruence relation on a monoid to a submonoid. -/ | ||
| @[to_additive "Restriction of a congruence relation on an `add_monoid` to an `add_submonoid`."] | ||
| def subtype (A : submonoid M) : con A := | ||
| ⟨λ x y, c x y, ⟨λ x, c.refl x, λ _ _, c.symm, λ _ _ _, c.trans⟩, |
There was a problem hiding this comment.
I've generalised the 'second isomorphism theorem for monoids' a bit based on this and added a 'second isomorphism theorem for sets' but I'm not really sure there's much point to their existences.
ChrisHughes24
added
the
ready-to-merge
anrddh
pushed a commit
to anrddh/mathlib
that referenced
this pull request
May 15, 2020
…ations (leanprover-community#1710) * add congruence.lean * add has_mul * add definition of congruence relation * minor changes * Tidy up second half of congruence.lean * tidying docstrings * tidying * constructive 3rd isom in setoid used in congruence * remove import * open namespaces earlier * responding to PR comments
anrddh
pushed a commit
to anrddh/mathlib
that referenced
this pull request
May 16, 2020
…ations (leanprover-community#1710) * add congruence.lean * add has_mul * add definition of congruence relation * minor changes * Tidy up second half of congruence.lean * tidying docstrings * tidying * constructive 3rd isom in setoid used in congruence * remove import * open namespaces earlier * responding to PR comments
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is the second half of
congruence.lean. Not sureto_submonoidshould be a coercion if it's not really to be used. I'll see if I can word the docstrings better when I get the chance.map_genshould be calledmapbut there's a different more importantmap:(TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list