Exactness of a pair

• For two maps f : M → N and g : N → P, with Zero P, Function.AddExact f g says that `Set.range f = Set.preimage {0}

• For two maps f : M → N and g : N → P, with One P, Function.Exact f g says that `Set.range f = Set.preimage {1}

• For linear maps f : M →ₗ[R] N and g : N →ₗ[R] P, Exact f g says that `range f = ker g``

TODO :

• add the cases of AddMonoidHom

• add the multiplicative case (Function.Exact will become Function.AddExact?)

def Function.Exact {M : Type u_1} {N : Type u_2} {P : Type u_3} (f : M → N) (g : N → P) [Zero P] : Prop

The maps f and g form an exact pair : g y = 0 iff y belongs to the image of f

Equations

• Function.Exact f g = ∀ (y : N), g y = 0 ↔ y ∈ Set.range f

theorem Function.Exact.comp_eq_zero {M : Type u_1} {N : Type u_2} {P : Type u_3} (f : M → N) (g : N → P) [Zero P] (h : Function.Exact f g) : g ∘ f = 0

theorem Function.Exact.linearMap_ker_eq {M : Type u_1} {N : Type u_2} {P : Type u_3} {R : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (hfg : Function.Exact ⇑f ⇑g) : LinearMap.ker g = LinearMap.range f

theorem Function.LinearMap.exact_iff {M : Type u_1} {N : Type u_2} {P : Type u_3} {R : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} : Function.Exact ⇑f ⇑g ↔ LinearMap.ker g = LinearMap.range f

theorem Function.Exact.linearMap_comp_eq_zero {M : Type u_1} {N : Type u_2} {P : Type u_3} {R : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : Function.Exact ⇑f ⇑g) : g ∘ₗ f = 0