Theorems · Theorem · group theory

AddSubmonoid.exists_addEquiv_eq_mgraph

∀ {H : Type u_2} {I : Type u_3} [inst : AddMonoid H] [inst_1 : AddMonoid I] {G : AddSubmonoid (H × I)},
  Function.Bijective (Prod.fst ∘ ⇑G.subtype) →
    Function.Bijective (Prod.snd ∘ ⇑G.subtype) → ∃ e, G = e.toAddMonoidHom.mgraph

Goursat's lemma for additive monoid isomorphisms. Let G ≤ H × I be a submonoid of a product of additive monoids. Assume that the natural maps from G to both factors are bijective. Then G is the graph of some isomorphism f : H ≃+ I.

Defined in

Mathlib.Algebra.Group.Graph

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddMonoidAddMonoid