Theorems · Theorem · group theory

MonoidHom.exists_mulEquiv_mrange_eq_mgraph

∀ {G : Type u_1} {H : Type u_2} {I : Type u_3} [inst : Monoid G] [inst_1 : Monoid H] [inst_2 : Monoid I]
  {f : G →* H × I},
  Function.Surjective (Prod.fst ∘ ⇑f) →
    Function.Surjective (Prod.snd ∘ ⇑f) →
      (∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) → ∃ e, MonoidHom.mrange f = e.toMonoidHom.mgraph

Line test for monoid isomorphisms. Let f : G → H × I be a homomorphism to a product of monoids. Assume that f is surjective on both factors and that the image of f intersects every "vertical line" {(h, i) | i : I} and every "horizontal line" {(h, i) | h : H} at most once. Then the image of f is the graph of some monoid isomorphism f' : H ≃ I.

Defined in

Mathlib.Algebra.Group.Graph

Cited by

2 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MonoidMonoidMonoid