# mathlibdocumentation

data.set.Union_lift

# Union lift #

This file defines set.Union_lift to glue together functions defined on each of a collection of sets to make a function on the Union of those sets.

## Main definitions #

• set.Union_lift - Given a Union of sets Union S, define a function on any subset of the Union by defining it on each component, and proving that it agrees on the intersections.
• set.lift_cover - Version of set.Union_lift for the special case that the sets cover the entire type.

## Main statements #

There are proofs of the obvious properties of Union_lift, i.e. what it does to elements of each of the sets in the Union, stated in different ways.

There are also three lemmas about Union_lift intended to aid with proving that Union_lift is a homomorphism when defined on a Union of substructures. There is one lemma each to show that constants, unary functions, or binary functions are preserved. These lemmas are:

*set.Union_lift_const *set.Union_lift_unary *set.Union_lift_binary

## Tags #

directed union, directed supremum, glue, gluing

@[nolint]
noncomputable def set.Union_lift {α : Type u_1} {ι : Type u_2} {β : Type u_3} (S : ι → set α) (f : Π (i : ι), (S i) → β) (hf : ∀ (i j : ι) (x : α) (hxi : x S i) (hxj : x S j), f i x, hxi⟩ = f j x, hxj⟩) (T : set α) (hT : T ) (x : T) :
β

Given a Union of sets Union S, define a function on the Union by defining it on each component, and proving that it agrees on the intersections.

Equations
@[simp]
theorem set.Union_lift_mk {α : Type u_1} {ι : Type u_2} {β : Type u_3} {S : ι → set α} {f : Π (i : ι), (S i) → β} {hf : ∀ (i j : ι) (x : α) (hxi : x S i) (hxj : x S j), f i x, hxi⟩ = f j x, hxj⟩} {T : set α} {hT : T } {i : ι} (x : (S i)) (hx : x T) :
hf T hT x, hx⟩ = f i x
@[simp]
theorem set.Union_lift_inclusion {α : Type u_1} {ι : Type u_2} {β : Type u_3} {S : ι → set α} {f : Π (i : ι), (S i) → β} {hf : ∀ (i j : ι) (x : α) (hxi : x S i) (hxj : x S j), f i x, hxi⟩ = f j x, hxj⟩} {T : set α} {hT : T } {i : ι} (x : (S i)) (h : S i T) :
hf T hT x) = f i x
theorem set.Union_lift_of_mem {α : Type u_1} {ι : Type u_2} {β : Type u_3} {S : ι → set α} {f : Π (i : ι), (S i) → β} {hf : ∀ (i j : ι) (x : α) (hxi : x S i) (hxj : x S j), f i x, hxi⟩ = f j x, hxj⟩} {T : set α} {hT : T } (x : T) {i : ι} (hx : x S i) :
hf T hT x = f i x, hx⟩
theorem set.Union_lift_const {α : Type u_1} {ι : Type u_2} {β : Type u_3} {S : ι → set α} {f : Π (i : ι), (S i) → β} {hf : ∀ (i j : ι) (x : α) (hxi : x S i) (hxj : x S j), f i x, hxi⟩ = f j x, hxj⟩} {T : set α} {hT : T } (c : T) (ci : Π (i : ι), (S i)) (hci : ∀ (i : ι), (ci i) = c) (cβ : β) (h : ∀ (i : ι), f i (ci i) =) :
hf T hT c =

Union_lift_const is useful for proving that Union_lift is a homomorphism of algebraic structures when defined on the Union of algebraic subobjects. For example, it could be used to prove that the lift of a collection of group homomorphisms on a union of subgroups preserves 1.

theorem set.Union_lift_unary {α : Type u_1} {ι : Type u_2} {β : Type u_3} {S : ι → set α} {f : Π (i : ι), (S i) → β} {hf : ∀ (i j : ι) (x : α) (hxi : x S i) (hxj : x S j), f i x, hxi⟩ = f j x, hxj⟩} {T : set α} (hT' : T = ) (u : T → T) (ui : Π (i : ι), (S i)(S i)) (hui : ∀ (i : ι) (x : (S i)), u x) = (ui i x)) (uβ : β → β) (h : ∀ (i : ι) (x : (S i)), f i (ui i x) = (f i x)) (x : T) :
hf T _ (u x) = f hf T _ x)

Union_lift_unary is useful for proving that Union_lift is a homomorphism of algebraic structures when defined on the Union of algebraic subobjects. For example, it could be used to prove that the lift of a collection of linear_maps on a union of submodules preserves scalar multiplication.

theorem set.Union_lift_binary {α : Type u_1} {ι : Type u_2} {β : Type u_3} {S : ι → set α} {f : Π (i : ι), (S i) → β} {hf : ∀ (i j : ι) (x : α) (hxi : x S i) (hxj : x S j), f i x, hxi⟩ = f j x, hxj⟩} {T : set α} (hT' : T = ) (dir : S) (op : T → T → T) (opi : Π (i : ι), (S i)(S i)(S i)) (hopi : ∀ (i : ι) (x y : (S i)), (opi i x y) = op x) y)) (opβ : β → β → β) (h : ∀ (i : ι) (x y : (S i)), f i (opi i x y) = opβ (f i x) (f i y)) (x y : T) :
hf T _ (op x y) = opβ f hf T _ x) f hf T _ y)

Union_lift_binary is useful for proving that Union_lift is a homomorphism of algebraic structures when defined on the Union of algebraic subobjects. For example, it could be used to prove that the lift of a collection of group homomorphisms on a union of subgroups preserves *.

noncomputable def set.lift_cover {α : Type u_1} {ι : Type u_2} {β : Type u_3} (S : ι → set α) (f : Π (i : ι), (S i) → β) (hf : ∀ (i j : ι) (x : α) (hxi : x S i) (hxj : x S j), f i x, hxi⟩ = f j x, hxj⟩) (hS : = set.univ) (a : α) :
β

Glue together functions defined on each of a collection S of sets that cover a type. See also set.Union_lift.

Equations
@[simp]
theorem set.lift_cover_coe {α : Type u_1} {ι : Type u_2} {β : Type u_3} {S : ι → set α} {f : Π (i : ι), (S i) → β} {hf : ∀ (i j : ι) (x : α) (hxi : x S i) (hxj : x S j), f i x, hxi⟩ = f j x, hxj⟩} {hS : = set.univ} {i : ι} (x : (S i)) :
hf hS x = f i x
theorem set.lift_cover_of_mem {α : Type u_1} {ι : Type u_2} {β : Type u_3} {S : ι → set α} {f : Π (i : ι), (S i) → β} {hf : ∀ (i j : ι) (x : α) (hxi : x S i) (hxj : x S j), f i x, hxi⟩ = f j x, hxj⟩} {hS : = set.univ} {i : ι} {x : α} (hx : x S i) :
hf hS x = f i x, hx⟩