Union lift

This file defines Set.iUnionLift 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.iUnionLift - Given a Union of sets iUnion 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.iUnionLift for the special case that the sets cover the entire type.

Main statements

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

There are also three lemmas about iUnionLift intended to aid with proving that iUnionLift 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.iUnionLift_const *Set.iUnionLift_unary *Set.iUnionLift_binary

Tags

directed union, directed supremum, glue, gluing

noncomputable def Set.iUnionLift {α : Type u_1} {ι : Sort u_2} {β : Sort 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.iUnion S → ↑T → β

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

Equations

• Set.iUnionLift S f x✝ T hT x = let i := Classical.indefiniteDescription (fun (x_1 : ι) => ↑x ∈ S x_1) ⋯; f ↑i { val := ↑x, property := ⋯ }

@[simp]

theorem Set.iUnionLift_mk {α : Type u_1} {ι : Sort u_3} {β : Sort 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.iUnion S} {i : ι} (x : ↑(S i)) (hx : ↑x ∈ T) : Set.iUnionLift S f hf T hT { val := ↑x, property := hx } = f i x

@[simp]

theorem Set.iUnionLift_inclusion {α : Type u_1} {ι : Sort u_3} {β : Sort 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.iUnion S} {i : ι} (x : ↑(S i)) (h : S i ⊆ T) : Set.iUnionLift S f hf T hT (Set.inclusion h x) = f i x

theorem Set.iUnionLift_of_mem {α : Type u_1} {ι : Sort u_3} {β : Sort 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.iUnion S} (x : ↑T) {i : ι} (hx : ↑x ∈ S i) : Set.iUnionLift S f hf T hT x = f i { val := ↑x, property := hx }

theorem Set.preimage_iUnionLift {α : Type u_1} {ι : Sort 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.iUnion S} (t : Set β) : Set.iUnionLift S f hf T hT ⁻¹' t = Set.inclusion hT ⁻¹' ⋃ (i : ι), Set.inclusion ⋯ '' (f i ⁻¹' t)

theorem Set.iUnionLift_const {α : Type u_1} {ι : Sort u_3} {β : Sort 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.iUnion S} (c : ↑T) (ci : (i : ι) → ↑(S i)) (hci : ∀ (i : ι), ↑(ci i) = ↑c) (cβ : β) (h : ∀ (i : ι), f i (ci i) = cβ) : Set.iUnionLift S f hf T hT c = cβ

iUnionLift_const is useful for proving that iUnionLift 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.iUnionLift_unary {α : Type u_1} {ι : Sort u_2} {β : Sort 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.iUnion S} (hT' : T = Set.iUnion 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.iUnionLift S f hf T ⋯ (u x) = uβ (Set.iUnionLift S f hf T ⋯ x)

iUnionLift_unary is useful for proving that iUnionLift 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.iUnionLift_binary {α : Type u_1} {ι : Sort u_2} {β : Sort 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.iUnion S} (hT' : T = Set.iUnion S) (dir : Directed (fun (x x_1 : Set α) => x ≤ x_1) 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 : ↑T) (y : ↑T) : Set.iUnionLift S f hf T ⋯ (op x y) = opβ (Set.iUnionLift S f hf T ⋯ x) (Set.iUnionLift S f hf T ⋯ y)

iUnionLift_binary is useful for proving that iUnionLift 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} {ι : Sort u_2} {β : Sort 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.iUnion S = Set.univ) (a : α) : β

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

Equations

• Set.liftCover S f hf hS a = Set.iUnionLift S f hf Set.univ ⋯ { val := a, property := trivial }

@[simp]

theorem Set.liftCover_coe {α : Type u_1} {ι : Sort u_3} {β : Sort 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.iUnion 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} {ι : Sort u_3} {β : Sort 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.iUnion 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_1} {ι : Sort 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.iUnion S = Set.univ} (t : Set β) : Set.liftCover S f hf hS ⁻¹' t = ⋃ (i : ι), Subtype.val '' (f i ⁻¹' t)