Theorems · Theorem · group theory

AddSubgroup.exists_eq_graph

∀ {H : Type u_2} {I : Type u_3} [inst : AddGroup H] [inst_1 : AddGroup I] {G : AddSubgroup (H × I)},
  Function.Bijective (Prod.fst ∘ ⇑G.subtype) → ∃ f, G = f.graph

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

0 results in Mathlib

Foundations

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

Assumes

AddGroupAddGroup