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

ink

noncomputable def Set.unionᵢLift {α : Type u_1} {ι : Type u_2} {β : Type u_3} (S : ι → Set α) (f : (i : ι) → ↑(S i) → β) : (∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i { val := x, property := hxi } = f j { val := x, property := hxj }) → (T : Set α) → T ⊆ Set.unionᵢ S → ↑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

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

ink

@[simp]

theorem Set.unionᵢLift_mk {α : Type u_1} {ι : Type u_3} {β : Type u_2} {S : ι → Set α} {f : (i : ι) → ↑(S i) → β} {hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i { val := x, property := hxi } = f j { val := x, property := hxj }} {T : Set α} {hT : T ⊆ Set.unionᵢ S} {i : ι} (x : ↑(S i)) (hx : ↑x ∈ T) : Set.unionᵢLift S f hf T hT { val := ↑x, property := hx } = f i x

ink

@[simp]

theorem Set.unionᵢLift_inclusion {α : Type u_1} {ι : Type u_3} {β : Type u_2} {S : ι → Set α} {f : (i : ι) → ↑(S i) → β} {hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i { val := x, property := hxi } = f j { val := x, property := 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

ink

theorem Set.unionᵢLift_of_mem {α : Type u_1} {ι : Type u_3} {β : Type u_2} {S : ι → Set α} {f : (i : ι) → ↑(S i) → β} {hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i { val := x, property := hxi } = f j { val := x, property := 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 { val := ↑x, property := hx }

ink

theorem Set.preimage_unionᵢLift {α : Type u_2} {ι : Type u_3} {β : Type u_1} {S : ι → Set α} {f : (i : ι) → ↑(S i) → β} {hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i { val := x, property := hxi } = f j { val := x, property := hxj }} {T : Set α} {hT : T ⊆ Set.unionᵢ S} (t : Set β) : Set.unionᵢLift S f hf T hT ⁻¹' t = Set.inclusion hT ⁻¹' Set.unionᵢ fun i => Set.inclusion (_ : S i ⊆ Set.unionᵢ fun i => S i) '' (f i ⁻¹' t)

ink

theorem Set.unionᵢLift_const {α : Type u_1} {ι : Type u_3} {β : Type u_2} {S : ι → Set α} {f : (i : ι) → ↑(S i) → β} {hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i { val := x, property := hxi } = f j { val := x, property := 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.

ink

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 { val := x, property := hxi } = f j { val := x, property := hxj }} {T : Set α} {hT : T ⊆ Set.unionᵢ S} (hT' : T = Set.unionᵢ S) (u : ↑T → ↑T) (ui : (i : ι) → ↑(S i) → ↑(S i)) (hui : ∀ (i : ι) (x : ↑(S i)), u (Set.inclusion (_ : S i ⊆ T) x) = Set.inclusion (_ : S i ⊆ T) (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 (_ : T ≤ Set.unionᵢ S) (u x) = uβ (Set.unionᵢLift S f hf T (_ : T ≤ Set.unionᵢ S) 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.

ink

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 { val := x, property := hxi } = f j { val := x, property := hxj }} {T : Set α} {hT : T ⊆ Set.unionᵢ S} (hT' : T = Set.unionᵢ S) (dir : Directed (fun x x_1 => x ≤ x_1) S) (op : ↑T → ↑T → ↑T) (opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)) (hopi : ∀ (i : ι) (x y : ↑(S i)), Set.inclusion (_ : S i ⊆ T) (opi i x y) = op (Set.inclusion (_ : S i ⊆ T) x) (Set.inclusion (_ : S i ⊆ T) y)) (opβ : β → β → β) (h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)) (x : ↑T) (y : ↑T) : Set.unionᵢLift S f hf T (_ : T ≤ Set.unionᵢ S) (op x y) = opβ (Set.unionᵢLift S f hf T (_ : T ≤ Set.unionᵢ S) x) (Set.unionᵢLift S f hf T (_ : T ≤ Set.unionᵢ S) 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 *.

ink

noncomputable def Set.liftCover {α : 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 { val := x, property := hxi } = f j { val := x, property := 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.liftCover S f hf hS a = Set.unionᵢLift S f hf Set.univ (_ : Set.univ ⊆ Set.unionᵢ S) { val := a, property := trivial }

ink

@[simp]

theorem Set.liftCover_coe {α : Type u_1} {ι : Type u_3} {β : Type u_2} {S : ι → Set α} {f : (i : ι) → ↑(S i) → β} {hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i { val := x, property := hxi } = f j { val := x, property := hxj }} {hS : Set.unionᵢ S = Set.univ} {i : ι} (x : ↑(S i)) : Set.liftCover S f hf hS ↑x = f i x

ink

theorem Set.liftCover_of_mem {α : Type u_1} {ι : Type u_3} {β : Type u_2} {S : ι → Set α} {f : (i : ι) → ↑(S i) → β} {hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i { val := x, property := hxi } = f j { val := x, property := hxj }} {hS : Set.unionᵢ S = Set.univ} {i : ι} {x : α} (hx : x ∈ S i) : Set.liftCover S f hf hS x = f i { val := x, property := hx }

ink

theorem Set.preimage_liftCover {α : Type u_2} {ι : Type u_3} {β : Type u_1} {S : ι → Set α} {f : (i : ι) → ↑(S i) → β} {hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i { val := x, property := hxi } = f j { val := x, property := hxj }} {hS : Set.unionᵢ S = Set.univ} (t : Set β) : Set.liftCover S f hf hS ⁻¹' t = Set.unionᵢ fun i => Subtype.val '' (f i ⁻¹' t)