Revision #2481 → #3131 · back to history
modifiedFirst isomorphism theorem (groups)d39bf4258ff4
| Field | From #2481 | To #3131 |
|---|
| note | Mathlib's `QuotientGroup.quotientKerEquivRange` gives the explicit isomorphism `G / ker φ ≃* range φ` for a group homomorphism `φ`. | Verified: `QuotientGroup.quotientKerEquivRange` gives `G ⧸ ker φ ≃* range φ` for a group homomorphism. |
modifiedSecond isomorphism theorem (groups)e66b97814d30
| Field | From #2481 | To #3131 |
|---|
| note | Mathlib's `QuotientGroup.quotientInfEquivProdNormalQuotient` is the classical second isomorphism `H/(H ∩ N) ≃* HN/N` for `N` normal. | Verified: `QuotientGroup.quotientInfEquivProdNormalQuotient` states `H/(H ∩ N) ≃* HN/N` for `N` normal. |
modifiedProjective linear group via second isomorphism theorema10c0c3bf4ae
| Field | From #2481 | To #3131 |
|---|
| note | Mathlib defines `PGL(n,R) := GL n R ⧸ Subgroup.center (GL n R)` directly but does not phrase its identification as an application of the second isomorphism theorem. | Mathlib defines `Matrix.ProjGenLinGroup` as `GL n R ⧸ Subgroup.center (GL n R)` directly, without deriving it as an instance of the second isomorphism theorem. |
modifiedThird isomorphism theorem and correspondence (groups)1b1b0a3d52ff
| Field | From #2481 | To #3131 |
|---|
| note | Mathlib's `QuotientGroup.quotientQuotientEquivQuotient` provides the canonical isomorphism `(G/N)/(M/N) ≃* G/M` when `N ≤ M`. | Verified: `QuotientGroup.quotientQuotientEquivQuotient` gives `(G/N)/(M/N) ≃* G/M` when `N ≤ M`. |
modifiedCorrespondence/lattice theorem (groups)a9b0df2ba636
| Field | From #2481 | To #3131 |
|---|
| note | Mathlib's `QuotientGroup.comapMk'OrderIso` is the lattice isomorphism between subgroups of `G/N` and subgroups of `G` containing `N`. | Verified: `QuotientGroup.comapMk'OrderIso` is the order isomorphism between subgroups of `G ⧸ N` and subgroups of `G` containing `N`. |
modifiedZassenhaus (butterfly) lemma4a1e463d2c83
| Field | From #2481 | To #3131 |
|---|
| note | Mathlib does not yet contain a formal statement of the Zassenhaus/butterfly lemma identifying the canonical isomorphism between the two refinement quotients arising from subgroups H, K of a group with normal subgroups H' ⊴ H, K' ⊴ K. | A semantic search turns up no formal Zassenhaus/butterfly-lemma statement in Mathlib. |
modifiedSplitting lemma24fe170de933
| Field | From #2481 | To #3131 |
|---|
| note | Mathlib formalizes splittings of short exact sequences via `CategoryTheory.ShortComplex.Splitting` in abelian categories; the classical equivalence of left/right splits invoked here is captured through this API rather than as a single named lemma. | Mathlib provides `CategoryTheory.ShortComplex.Splitting` in abelian categories, encoding the classical left/right split equivalence through the general splitting API rather than as a single named lemma. |
modifiedNine lemma5a6bbbfffb71
| Field | From #2481 | To #3131 |
|---|
| note | Mathlib does not yet contain a general statement of the 3×3 (nine) lemma for abelian categories. | Mathlib has snake- and four-lemma infrastructure in `CategoryTheory.Abelian.DiagramLemmas` but no explicit 3×3 (nine) lemma statement. |
modifiedFirst isomorphism theorem (rings)f65cf476c5f0
| Field | From #2481 | To #3131 |
|---|
| note | Mathlib's `RingHom.quotientKerEquivRange` gives `R/ker f ≃+* f.range` for a ring homomorphism `f`. | Verified: `RingHom.quotientKerEquivRange` gives `R ⧸ ker f ≃+* f.range` for a ring homomorphism. |
modifiedSecond isomorphism theorem (rings)63dfdf28b082
| Field | From #2481 | To #3131 |
|---|
| note | Mathlib's `RingCon.comapQuotientEquivRange` is labelled as the second isomorphism theorem for rings via ring congruences, generalizing the classical `(S+I)/I ≅ S/(S∩I)` statement. | Verified: `RingCon.comapQuotientEquivRange` phrases the second isomorphism theorem for rings via ring congruences, generalizing the classical `(S+I)/I ≅ S/(S∩I)`. |
modifiedThird isomorphism theorem and correspondence (rings)9b3bf6d35916
| Field | From #2481 | To #3131 |
|---|
| note | Mathlib's `DoubleQuot.quotQuotEquivQuotOfLE` is the third isomorphism theorem for rings: `(R/I)/(J/I) ≃+* R/J` when `I ≤ J`. | Verified: `DoubleQuot.quotQuotEquivQuotOfLE` provides `(R ⧸ I) ⧸ (J.map _) ≃+* R ⧸ J` when `I ≤ J`. |
modifiedCorrespondence theorem (rings)232c0192081c
| Field | From #2481 | To #3131 |
|---|
| note | Mathlib's `Ideal.relIsoOfSurjective` gives the order isomorphism `Ideal S ≃o {p : Ideal R // comap f ⊥ ≤ p}` for a surjective ring homomorphism. | Verified: `Ideal.relIsoOfSurjective` gives the order iso `Ideal S ≃o {p : Ideal R // comap f ⊥ ≤ p}` for a surjective ring homomorphism. |
modifiedFirst isomorphism theorem (modules)c788b3d932ad
| Field | From #2481 | To #3131 |
|---|
| note | Mathlib's `LinearMap.quotKerEquivRange` provides the canonical `M/ker f ≃ₗ[R] range f` for a linear map `f`. | Verified: `LinearMap.quotKerEquivRange` provides `M ⧸ ker f ≃ₗ[R] range f` for a linear map `f`. |
modifiedSecond isomorphism theorem (modules)6bc9a062290a
| Field | From #2481 | To #3131 |
|---|
| note | Mathlib's `LinearMap.quotientInfEquivSupQuotient` is the second isomorphism theorem for modules: `p / (p ⊓ p') ≃ₗ (p ⊔ p') / p'`. | Verified: `LinearMap.quotientInfEquivSupQuotient` gives `p ⧸ (p ⊓ p') ≃ₗ (p ⊔ p') ⧸ p'`. |
modifiedThird isomorphism theorem and correspondence (modules)bdaff56b2e40
| Field | From #2481 | To #3131 |
|---|
| note | Mathlib's `Submodule.quotientQuotientEquivQuotient` provides `(M/S)/(T/S) ≃ₗ[R] M/T` when `S ≤ T`. | Verified: `Submodule.quotientQuotientEquivQuotient` gives `(M/S)/(T/S) ≃ₗ[R] M/T` when `S ≤ T`. |
modifiedCorrespondence theorem (modules)fabb9397e70a
| Field | From #2481 | To #3131 |
|---|
| note | Mathlib's `Submodule.comapMkQRelIso` gives the order isomorphism `Submodule R (M ⧸ p) ≃o Set.Ici p` between submodules of `M/p` and submodules of `M` containing `p`. | Verified: `Submodule.comapMkQRelIso` provides the order iso `Submodule R (M ⧸ p) ≃o Set.Ici p`. |
modifiedRank–nullity theorem (modules section)fb0253f15bca
| Field | From #2481 | To #3131 |
|---|
| note | Mathlib's `Submodule.finrank_quotient_add_finrank` states `finrank (M ⧸ p) + finrank p = finrank M` for finite-dimensional vector spaces, the rank–nullity identity invoked here. | Verified: `Submodule.finrank_quotient_add_finrank` gives `finrank (M ⧸ p) + finrank p = finrank M` for finite-dimensional vector spaces. |
modifiedCongruence on an algebrac9b3ce4c43d4
| Field | From #2481 | To #3131 |
|---|
| note | Mathlib has structure-specific congruences (`Con` for magmas/monoids, `AddCon`, `RingCon`) and `Setoid`, but no fully general universal-algebra congruence definition. | Mathlib has structure-specific congruences (`Con`, `AddCon`, `RingCon`) and `Setoid`, but no general universal-algebra congruence framework. |
modifiedFirst isomorphism theorem (universal algebra)d8b7fb0b9793
| Field | From #2481 | To #3131 |
|---|
| note | Mathlib formalizes the first isomorphism theorem for `Con`/`RingCon`/`Setoid` separately but lacks a single universal-algebra statement. | Verified: `Con.quotientKerEquivRange` and analogues (`RingCon`, `Setoid`) exist, but Mathlib has no universal-algebra-level statement. |
modifiedSecond isomorphism theorem (universal algebra)7651002936e1
| Field | From #2481 | To #3131 |
|---|
| note | Only structure-specific versions (e.g. `Con.comapQuotientEquiv`, `RingCon.comapQuotientEquivRange`, `LinearMap.quotientInfEquivSupQuotient`) exist; no general universal-algebra version is in Mathlib. | Only structure-specific versions (`Con.comapQuotientEquiv`, `RingCon.comapQuotientEquivRange`, `LinearMap.quotientInfEquivSupQuotient`) are formalized. |
modifiedThird isomorphism theorem (universal algebra)cbcd76fae47e
| Field | From #2481 | To #3131 |
|---|
| note | Mathlib has `Setoid.quotientQuotientEquivQuotient` plus the `Con` and `RingCon` variants, but no statement at the level of universal algebra. | Verified: `Setoid.quotientQuotientEquivQuotient` plus `Con`/`RingCon` variants exist, but no universal-algebra statement. |
modifiedCorrespondence theorem (universal algebra)f07ac405245b
| Field | From #2481 | To #3131 |
|---|
| mathlib.decl | — | Con.correspondence |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.GroupTheory.Congruence.Hom |
| note | Mathlib has correspondence/lattice theorems for subgroups, ideals, and submodules but no general bijection between congruences containing a given congruence and congruences on the quotient algebra. | Verified: `Con.correspondence` gives `{d // c ≤ d} ≃o Con c.Quotient` for magma congruences (with `AddCon`/`RingCon` analogues), but Mathlib has no fully universal-algebra correspondence theorem. |
| status | not_formalized | partial |
addedQuotient algebra by a congruence52997c6710e7