Documentation

Mathlib.Data.Set.UnionLift

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 #

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

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
  • One or more equations did not get rendered due to their size.
Instances For
    @[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 (_ : S i ⋃ (i : ι), S i) '' (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) = ) :
    Set.iUnionLift S f hf T hT 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 : 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.iUnionLift S f hf T (_ : T Set.iUnion S) (u x) = (Set.iUnionLift S f hf T (_ : T Set.iUnion S) 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 => 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.iUnionLift S f hf T (_ : T Set.iUnion S) (op x y) = opβ (Set.iUnionLift S f hf T (_ : T Set.iUnion S) x) (Set.iUnionLift S f hf T (_ : T Set.iUnion S) 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
    Instances For
      @[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)