Documentation

Mathlib.Data.Set.UnionLift

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

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ᵢ STβ

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.
@[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
@[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
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 }
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)
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) = ) :
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 { val := x, property := hxi } = f j { val := x, property := hxj }} {T : Set α} {hT : T Set.unionᵢ S} (hT' : T = Set.unionᵢ S) (u : TT) (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) = (f i x)) (x : T) :
Set.unionᵢLift S f hf T (_ : T Set.unionᵢ S) (u x) = (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.

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 : TTT) (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 *.

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