Theorems · Theorem · group theory

AddSubmonoid.exists_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) → ∃ f, G = f.mgraph

Vertical line test for additive monoid homomorphisms. Let G ≤ H × I be a submonoid of a product of monoids. Assume that G surjects onto the first factor and G intersects every "vertical line" {(h, i) | i : I} at most once. Then G is the graph of some monoid homomorphism f : H → I.

Defined in

Mathlib.Algebra.Group.Graph

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddMonoidAddMonoid