Theorems · Theorem · category theory

Function.Exact.iff_addMonoidHom_rangeRestrict

∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : AddGroup M] [inst_1 : AddGroup N] [inst_2 : AddGroup P]
  {f : M →+ N} {g : N →+ P}, Function.Exact ⇑f ⇑g ↔ Function.Exact ⇑f.range.subtype ⇑g.rangeRestrict

Two maps f : M →+ N and g : N →+ P are exact if and only if the induced maps AddMonoidHom.range f → N → AddMonoidHom.range g are exact.

Defined in

Mathlib.Algebra.Exact.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddGroupAddGroupAddGroup