mathlib documentation

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 #

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 set.Union S) (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 set.Union S} {i : ι} (x : (S i)) (hx : x T) :
set.Union_lift S f 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 set.Union S} {i : ι} (x : (S i)) (h : S i T) :
set.Union_lift S f hf T hT (set.inclusion h 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 set.Union S} (x : T) {i : ι} (hx : x S i) :
set.Union_lift S f 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 set.Union S} (c : T) (ci : Π (i : ι), (S i)) (hci : ∀ (i : ι), (ci i) = c) (cβ : β) (h : ∀ (i : ι), f i (ci i) =) :
set.Union_lift S f 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 = set.Union S) (u : T → T) (ui : Π (i : ι), (S i)(S i)) (hui : ∀ (i : ι) (x : (S i)), u (set.inclusion _ x) = set.inclusion _ (ui i x)) (uβ : β → β) (h : ∀ (i : ι) (x : (S i)), f i (ui i x) = (f i x)) (x : T) :
set.Union_lift S f hf T _ (u x) = (set.Union_lift S 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 = set.Union S) (dir : directed has_le.le S) (op : T → T → T) (opi : Π (i : ι), (S i)(S i)(S i)) (hopi : ∀ (i : ι) (x y : (S i)), set.inclusion _ (opi i x y) = op (set.inclusion _ x) (set.inclusion _ y)) (opβ : β → β → β) (h : ∀ (i : ι) (x y : (S i)), f i (opi i x y) = opβ (f i x) (f i y)) (x y : T) :
set.Union_lift S f hf T _ (op x y) = opβ (set.Union_lift S f hf T _ x) (set.Union_lift S 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.Union S = 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.Union S = set.univ} {i : ι} (x : (S i)) :
set.lift_cover S f 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.Union S = set.univ} {i : ι} {x : α} (hx : x S i) :
set.lift_cover S f hf hS x = f i x, hx⟩