Disjoint sums and options over ZF sets

This file defines the disjoint sum A ⊎ B of two ZFSets as a subtype, with constructors, eliminators, and an equivalence to the type-level sum. It also develops Option S together with bijections relating it to _root_.Option and a lifting of functions to options.

def ZFSet.Sum (A B : ZFSet.{u_1}) : Type (u_1 + 1)

Equations

• (A ⊎ B) = ↥({↑ZFSet.ZFBool.false}.prod A ∪ {↑ZFSet.ZFBool.true}.prod B)

def ZFSet.«term_⊎_» : Lean.TrailingParserDescr

Equations

• ZFSet.«term_⊎_» = Lean.ParserDescr.trailingNode `ZFSet.«term_⊎_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊎ ") (Lean.ParserDescr.cat `term 50))

def ZFSet.Sum.inl {A B : ZFSet.{u_1}} (a : ↥A) : A ⊎ B

Equations

• ZFSet.Sum.inl a = ⟨(↑ZFSet.ZFBool.false).pair ↑a, ⋯⟩

def ZFSet.Sum.inr {A B : ZFSet.{u_1}} (b : ↥B) : A ⊎ B

Equations

• ZFSet.Sum.inr b = ⟨(↑ZFSet.ZFBool.true).pair ↑b, ⋯⟩

theorem ZFSet.Sum.inl.injEq {A B : ZFSet.{u_1}} {x y : ↥A} : inl x = inl y ↔ x = y

theorem ZFSet.Sum.inr.injEq {A B : ZFSet.{u_1}} {x y : ↥B} : inr x = inr y ↔ x = y

theorem ZFSet.Sum.cases {A B : ZFSet.{u_1}} (x : A ⊎ B) : (↑x).π₂ ∈ A ∨ (↑x).π₂ ∈ B

noncomputable def ZFSet.Sum.casesOn {A B : ZFSet.{u}} {motive : A ⊎ B → Sort v} (x : A ⊎ B) (inl : (val : ↥A) → motive (inl val)) (inr : (val : ↥B) → motive (inr val)) : motive x

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ZFSet.Sum.casesOn_of_inl {A B : ZFSet.{u_2}} {motive : A ⊎ B → Sort u_1} (a : ↥A) (inl_case : (val : ↥A) → motive (inl val)) (inr_case : (val : ↥B) → motive (inr val)) : casesOn (inl a) inl_case inr_case = inl_case a

@[simp]

theorem ZFSet.Sum.casesOn_of_inr {A B : ZFSet.{u_2}} {motive : A ⊎ B → Sort u_1} (a : ↥B) (inl_case : (val : ↥A) → motive (inl val)) (inr_case : (val : ↥B) → motive (inr val)) : casesOn (inr a) inl_case inr_case = inr_case a

theorem ZFSet.Sum.casesOn_unique {A B : ZFSet.{u_2}} {motive : A ⊎ B → Sort u_1} (inl_case : (a : ↥A) → motive (inl a)) (inr_case : (b : ↥B) → motive (inr b)) (g : (x : A ⊎ B) → motive x) (hinl : ∀ (a : ↥A), g (inl a) = inl_case a) (hinr : ∀ (b : ↥B), g (inr b) = inr_case b) (x : A ⊎ B) : g x = casesOn x inl_case inr_case

Uniqueness half of the universal property of the disjoint sum: casesOn is the only family agreeing with inl_case along inl and with inr_case along inr.

noncomputable def ZFSet.Sum.equivSum {A B : ZFSet.{u_1}} : A ⊎ B ≃ ↥A ⊕ ↥B

Equations

• One or more equations did not get rendered due to their size.

Set-level universal property of the coproduct

Everything above states the disjoint sum at the type level: A ⊎ B is a Lean subtype and casesOn eliminates into a Lean family. This section states the same universal property inside the model: the objects are ZFSets, the arrows are elements of funs, and composition is ZFSet.composition.

def ZFSet.Sum.toZFSet (A B : ZFSet.{u_1}) : ZFSet.{u_1}

The underlying ZFSet carrier of the disjoint sum: A ⊎ B is {x // x ∈ toZFSet A B}.

Equations

• ZFSet.Sum.toZFSet A B = {↑ZFSet.ZFBool.false}.prod A ∪ {↑ZFSet.ZFBool.true}.prod B

theorem ZFSet.Sum.sum_eq_subtype_toZFSet {A B : ZFSet.{u_1}} : (A ⊎ B) = ↥(toZFSet A B)

theorem ZFSet.Sum.pair_false_mem_toZFSet {A B a : ZFSet.{u_1}} (ha : a ∈ A) : (↑ZFBool.false).pair a ∈ toZFSet A B

theorem ZFSet.Sum.pair_true_mem_toZFSet {A B b : ZFSet.{u_1}} (hb : b ∈ B) : (↑ZFBool.true).pair b ∈ toZFSet A B

theorem ZFSet.Sum.mem_left_of_toZFSet {A B z : ZFSet.{u_1}} (hz : z ∈ toZFSet A B) (h : z.π₁ = ↑ZFBool.false) : z.π₂ ∈ A

An element of toZFSet A B tagged by false has its second projection in A.

theorem ZFSet.Sum.mem_right_of_toZFSet {A B z : ZFSet.{u_1}} (hz : z ∈ toZFSet A B) (h : z.π₁ ≠ ↑ZFBool.false) : z.π₂ ∈ B

An element of toZFSet A B not tagged by false has its second projection in B.

noncomputable def ZFSet.Sum.inlFun (A B : ZFSet.{u_1}) : ZFSet.{u_1}

The left injection A → A ⊎ B, as a set-level function.

Equations

• ZFSet.Sum.inlFun A B = A.lambda (ZFSet.Sum.toZFSet A B) fun (a : ZFSet.{?u.1}) => (↑ZFSet.ZFBool.false).pair a

noncomputable def ZFSet.Sum.inrFun (A B : ZFSet.{u_1}) : ZFSet.{u_1}

The right injection B → A ⊎ B, as a set-level function.

Equations

• ZFSet.Sum.inrFun A B = B.lambda (ZFSet.Sum.toZFSet A B) fun (a : ZFSet.{?u.1}) => (↑ZFSet.ZFBool.true).pair a

theorem ZFSet.Sum.inlFun_is_func {A B : ZFSet.{u_1}} : A.IsFunc (toZFSet A B) (inlFun A B)

theorem ZFSet.Sum.inrFun_is_func {A B : ZFSet.{u_1}} : B.IsFunc (toZFSet A B) (inrFun A B)

noncomputable def ZFSet.Sum.coprod {A B X : ZFSet.{u_1}} (f g : ZFSet.{u_1}) (hf : A.IsFunc X f := by zfun) (hg : B.IsFunc X g := by zfun) : ZFSet.{u_1}

The mediating map [f, g] : A ⊎ B → X of the coproduct: it applies f to the elements tagged by false and g to those tagged by true.

Equations

• One or more equations did not get rendered due to their size.

theorem ZFSet.Sum.coprod_is_func {A B X f g : ZFSet.{u_1}} (hf : A.IsFunc X f) (hg : B.IsFunc X g) : (toZFSet A B).IsFunc X (coprod f g hf hg)

theorem ZFSet.Sum.coprod_is_pfunc {A B X f g : ZFSet.{u_1}} (hf : A.IsFunc X f) (hg : B.IsFunc X g) : (coprod f g hf hg).IsPFunc (toZFSet A B) X

[f, g] as a partial function, so that fapply can be applied to it without re-running the zpfun search on the (large) body of coprod.

theorem ZFSet.Sum.coprod_of_inl {A B X f g : ZFSet.{u_1}} (hf : A.IsFunc X f) (hg : B.IsFunc X g) {a : ZFSet.{u_1}} (ha : a ∈ A) : @ᶻ(coprod f g hf hg) ⋯ ⟨(↑ZFBool.false).pair a, ⋯⟩ = @ᶻf ⋯ ⟨a, ⋯⟩

[f, g] computes with f on the left summand.

theorem ZFSet.Sum.coprod_of_inr {A B X f g : ZFSet.{u_1}} (hf : A.IsFunc X f) (hg : B.IsFunc X g) {b : ZFSet.{u_1}} (hb : b ∈ B) : @ᶻ(coprod f g hf hg) ⋯ ⟨(↑ZFBool.true).pair b, ⋯⟩ = @ᶻg ⋯ ⟨b, ⋯⟩

[f, g] computes with g on the right summand.

theorem ZFSet.Sum.fapply_inlFun {A B x : ZFSet.{u_1}} (hx : x ∈ A) : @ᶻ(inlFun A B) ⋯ ⟨x, ⋯⟩ = ⟨(↑ZFBool.false).pair x, ⋯⟩

theorem ZFSet.Sum.coprod_comp_inl {A B X f g : ZFSet.{u_1}} (hf : A.IsFunc X f) (hg : B.IsFunc X g) : (coprod f g hf hg ∘ᶻ inlFun A B) ⋯ ⋯ = f

theorem ZFSet.Sum.fapply_inrFun {A B x : ZFSet.{u_1}} (hx : x ∈ B) : @ᶻ(inrFun A B) ⋯ ⟨x, ⋯⟩ = ⟨(↑ZFBool.true).pair x, ⋯⟩

theorem ZFSet.Sum.eta_of_toZFSet {A B z : ZFSet.{u_1}} (hz : z ∈ toZFSet A B) : z = z.π₁.pair z.π₂

theorem ZFSet.Sum.exists_repr_of_toZFSet {A B z : ZFSet.{u_1}} (hz : z ∈ toZFSet A B) : (∃ a ∈ A, z = (↑ZFBool.false).pair a) ∨ ∃ b ∈ B, z = (↑ZFBool.true).pair b

theorem ZFSet.Sum.coprod_comp_inr {A B X f g : ZFSet.{u_1}} (hf : A.IsFunc X f) (hg : B.IsFunc X g) : (coprod f g hf hg ∘ᶻ inrFun A B) ⋯ ⋯ = g

theorem ZFSet.Sum.coprod_unique {A B X f g m : ZFSet.{u_1}} (hf : A.IsFunc X f) (hg : B.IsFunc X g) (hm : (toZFSet A B).IsFunc X m) (hl : (m ∘ᶻ inlFun A B) hm ⋯ = f) (hr : (m ∘ᶻ inrFun A B) hm ⋯ = g) : m = coprod f g hf hg

theorem ZFSet.Sum.funs_coprod_universal {A B X f g : ZFSet.{u_1}} (hf : f ∈ A.funs X) (hg : g ∈ B.funs X) : ∃! m : ZFSet.{u_1}, m ∈ (toZFSet A B).funs X ∧ m.composition (inlFun A B) A (toZFSet A B) X = f ∧ m.composition (inrFun A B) B (toZFSet A B) X = g

Set-level universal property of the coproduct. For f ∈ A.funs X and g ∈ B.funs X there is a unique m ∈ (toZFSet A B).funs X whose restrictions along the two injections inlFun/inrFun are f and g. The mediating map is coprod f g.

This is the statement of Sum.casesOn / Sum.casesOn_unique transported inside the model: objects are ZFSets, arrows are elements of funs, composition is ZFSet.composition.

@[reducible]

def ZFSet.Option (S : ZFSet.{u_1}) : Type (u_1 + 1)

Option S is the disjoint sum {∅} ⊎ S. Marked reducible so that the two spellings stay interchangeable under rw and simp.

Equations

• S.Option = ({∅} ⊎ S)

instance ZFSet.instNonemptyOption {T : ZFSet.{u_1}} : Nonempty T.Option

@[reducible, inline]

abbrev ZFSet.Option.none {S : ZFSet.{u_1}} : S.Option

Equations

• ZFSet.Option.none = ZFSet.Sum.inl ⟨∅, ZFSet.Option.none._proof_1⟩

@[reducible, inline]

abbrev ZFSet.Option.some {S : ZFSet.{u_1}} (x : ↥S) : S.Option

Equations

• ZFSet.Option.some x = ZFSet.Sum.inr x

theorem ZFSet.Option.some_ne_none {S : ZFSet.{u_1}} (x : ↥S) : some x ≠ none

theorem ZFSet.Option.casesOn {S : ZFSet.{u_1}} (x : S.Option) : x = none ∨ ∃ (y : ↥S), x = some y

theorem ZFSet.Option.inl_eq_none {S : ZFSet.{u_1}} (a : ↥{∅}) : Sum.inl a = none

The left summand of Option S is a singleton: every inl is none.

noncomputable def ZFSet.Option.elim {S : ZFSet.{u_1}} {motive : S.Option → Sort v} (x : S.Option) (none_case : motive none) (some_case : (y : ↥S) → motive (some y)) : motive x

Cases elimination for Option, the data-level counterpart of the disjunction Option.casesOn. It is Sum.casesOn on {∅} ⊎ S, using inl_eq_none to collapse the left summand.

Equations

• ZFSet.Option.elim x none_case some_case = ZFSet.Sum.casesOn x (fun (a : ↥{∅}) => ⋯.mpr none_case) some_case

@[simp]

theorem ZFSet.Option.elim_of_none {S : ZFSet.{u_2}} {motive : S.Option → Sort u_1} (none_case : motive none) (some_case : (y : ↥S) → motive (some y)) : elim none none_case some_case = none_case

Computation rule of elim on none.

@[simp]

theorem ZFSet.Option.elim_of_some {S : ZFSet.{u_2}} {motive : S.Option → Sort u_1} (none_case : motive none) (some_case : (y : ↥S) → motive (some y)) (y : ↥S) : elim (some y) none_case some_case = some_case y

Computation rule of elim on some.

theorem ZFSet.Option.elim_unique {S : ZFSet.{u_2}} {motive : S.Option → Sort u_1} (none_case : motive none) (some_case : (y : ↥S) → motive (some y)) (g : (x : S.Option) → motive x) (hnone : g none = none_case) (hsome : ∀ (y : ↥S), g (some y) = some_case y) (x : S.Option) : g x = elim x none_case some_case

Uniqueness half of the universal property of Option: elim is the only family agreeing with none_case on none and with some_case along some.

@[reducible, inline]

noncomputable abbrev ZFSet.Option.the {S : ZFSet.{u_1}} (S_nemp : S ≠ ∅) (x : S.Option) : ↥S

Equations

• ZFSet.Option.the S_nemp x = if isNone : x = ZFSet.Option.none then ⟨(fun (x : ZFSet.{?u.1}) => Classical.epsilon fun (z : ZFSet.{?u.1}) => z ∈ x) S, ⋯⟩ else Classical.choose ⋯

theorem ZFSet.Option.some.injEq {T : ZFSet.{u_1}} {x y : ↥T} : some x = some y ↔ x = y

theorem ZFSet.Option.ne_none_is_some {T : ZFSet.{u_1}} (x : T.Option) : x ≠ none → ∃ (y : ↥T), x = some y

noncomputable def ZFSet.Option.EmbeddingZFOptionOption {T : ZFSet.{u_1}} : T.Option ↪ _root_.Option ↥T

Equations

• ZFSet.Option.EmbeddingZFOptionOption = { toFun := ZFSet.Option.into✝, inj' := ⋯ }

noncomputable def ZFSet.Option.instEquivZFOptionOption {T : ZFSet.{u_1}} : T.Option ≃ _root_.Option ↥T

Equations

• ZFSet.Option.instEquivZFOptionOption = { toFun := ZFSet.Option.into✝, invFun := Function.invFun ZFSet.Option.into✝, left_inv := ⋯, right_inv := ⋯ }

def ZFSet.Option.EmbeddingOptionZFOption {T : ZFSet.{u_1}} : _root_.Option ↥T ↪ T.Option

Equations

• ZFSet.Option.EmbeddingOptionZFOption = { toFun := ZFSet.Option.outof✝, inj' := ⋯ }

noncomputable def ZFSet.Option.instEquivOptionZFOption {T : ZFSet.{u_1}} : _root_.Option ↥T ≃ T.Option

Equations

• ZFSet.Option.instEquivOptionZFOption = { toFun := ZFSet.Option.outof✝, invFun := Function.invFun ZFSet.Option.outof✝, left_inv := ⋯, right_inv := ⋯ }

@[reducible, inline]

abbrev ZFSet.Option.toZFSet (T : ZFSet.{u_1}) : ZFSet.{u_1}

Equations

• ZFSet.Option.toZFSet T = {↑ZFSet.ZFBool.false}.prod {∅} ∪ {↑ZFSet.ZFBool.true}.prod T

noncomputable def ZFSet.Option.flift {A B : ZFSet.{u_1}} (f : ZFSet.{u_1}) (hf : A.IsFunc B f := by zfun) : { f' : ZFSet.{u_1} // (toZFSet A).IsFunc (toZFSet B) f' }

Equations

• One or more equations did not get rendered due to their size.

theorem ZFSet.Option.flift_bijective {f A B : ZFSet.{u_1}} (hf : A.IsFunc B f) : (↑(flift f hf)).IsBijective ⋯ ↔ f.IsBijective hf