TODO: Use Pointed (the category of pointed types) in Mathlib.

class IsPointedMap {X : Type u_1} {Y : Type u_2} [Inhabited X] [Inhabited Y] (f : X → Y) : Prop

IsPointedMap

• map_default : f default = default

theorem IsPointedMap.default_mem_image_of_default_mem {X : Type u_1} {Y : Type u_2} [Inhabited X] [Inhabited Y] (f : X → Y) [IsPointedMap f] {A : Set X} : default ∈ A → default ∈ f '' A

theorem IsPointedMap.default_mem_preimage_default {X : Type u_1} {Y : Type u_2} [Inhabited X] [Inhabited Y] (f : X → Y) [IsPointedMap f] : default ∈ f ⁻¹' {default}

theorem IsPointedMap.default_subset_preimage_default {X : Type u_1} {Y : Type u_2} [Inhabited X] [Inhabited Y] (f : X → Y) [IsPointedMap f] : {default} ⊆ f ⁻¹' {default}

theorem IsPointedMap.default_eq_image_preimage_default {X : Type u_1} {Y : Type u_2} [Inhabited X] [Inhabited Y] (f : X → Y) [IsPointedMap f] : {default} = f '' f ⁻¹' {default}

def ExactSeq.IsExactAt {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Inhabited Z] (f : X → Y) (g : Y → Z) : Prop

IsExactAt

Equations

• ExactSeq.IsExactAt f g = (g ⁻¹' {default} = Set.range f)

theorem ExactSeq.isExactAt_of_ker_supset_im_of_ker_subset_im {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Inhabited X] [Inhabited Y] [Inhabited Z] {f : X → Y} {g : Y → Z} [IsPointedMap f] [IsPointedMap g] (hsup : ∀ (y : Y), (∃ (x : X), f x = y) → g y = default) (hsub : ∀ (y : Y), g y = default → ∃ (x : X), f x = y) : IsExactAt f g

Given an exact sequence A --a-> B --b-> C --c-> D --d-> E of five pointed sets, if a is surjective and d is injective, then C = 0. proof.

• Ker b = Im a = B (since a is surjective)
• Hence Im b = 0
• 0 = Ker d = Im c (since d is injective)
• Hence Ker c = C
• Use Ker c = Im b to conclude C = 0.

theorem ExactSeq.unique_mid_of_five {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} {E : Type u_5} [Inhabited A] [Inhabited B] [Inhabited C] [Inhabited D] [Inhabited E] (a : A → B) (b : B → C) (c : C → D) (d : D → E) [IsPointedMap a] [IsPointedMap b] [IsPointedMap c] [IsPointedMap d] (a_surj : Function.Surjective a) (d_inj : Function.Injective d) (exb : IsExactAt a b) (exc : IsExactAt b c) (exd : IsExactAt c d) : Nonempty (Unique C)

C = {0} if there is an exact sequence A --a-> B --b-> C --c-> D --d-> E of five pointed sets such that a is surjective and d is injective.