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

source

@[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

set.Union_lift S f hf T hT x = let i : {x_1 // ↑x ∈ S x_1} := classical.indefinite_description (λ (x_1 : ι), ↑x ∈ S x_1) _ in f ↑i ⟨↑x, _⟩

source

@[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

source

@[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

source

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⟩

source

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) = cβ) :

set.Union_lift S f hf T hT c = 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.

source

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) = uβ (f i x)) (x : ↥T) :

set.Union_lift S f hf T _ (u x) = uβ (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.

source

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 *.

source

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

set.lift_cover S f hf hS a = set.Union_lift S f hf set.univ _ ⟨a, trivial⟩

source

@[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

source

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⟩