Mathlib.Data.Set.UnionLift

Module docstring

{"# 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 "}

Set.iUnionLift definition

 (S : ι → Set α) (f : ∀ i, S i → β) (_ : ∀ (i j) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩)
  (T : Set α) (hT : T ⊆ iUnion S) (x : T) : β

Full source

/-- 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. -/
@[nolint unusedArguments]
noncomputable def iUnionLift (S : ι → Set α) (f : ∀ i, S i → β)
    (_ : ∀ (i j) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩) (T : Set α)
    (hT : T ⊆ iUnion S) (x : T) : β :=
  let i := Classical.indefiniteDescription _ (mem_iUnion.1 (hT x.prop))
  f i ⟨x, i.prop⟩

Lifting functions to a union of sets

Informal description

Given an indexed family of sets $ S : \iota \to \text{Set } \alpha $, a family of functions $ f_i : S_i \to \beta $ for each $ i \in \iota $ that agree on pairwise intersections (i.e., for any $ i, j \in \iota $ and $ x \in S_i \cap S_j $, $ f_i(x) = f_j(x) $), a subset $ T \subseteq \bigcup_i S_i $, and an element $ x \in T $, the function `Set.iUnionLift` constructs a function from $ T $ to $ \beta $ by lifting the functions $ f_i $ to the union. Specifically, for $ x \in T $, it selects an index $ i $ such that $ x \in S_i $ and returns $ f_i(x) $.

Set.iUnionLift_mk theorem

{i : ι} (x : S i) (hx : (x : α) ∈ T) : iUnionLift S f hf T hT ⟨x, hx⟩ = f i x

Full source

@[simp]
theorem iUnionLift_mk {i : ι} (x : S i) (hx : (x : α) ∈ T) :
    iUnionLift S f hf T hT ⟨x, hx⟩ = f i x := hf _ i x _ _

Value of Union Lift on Elements from Component Sets

Informal description

Let $S : \iota \to \text{Set } \alpha$ be an indexed family of sets, and let $f_i : S_i \to \beta$ be a family of functions for each $i \in \iota$ that agree on pairwise intersections (i.e., for any $i, j \in \iota$ and $x \in S_i \cap S_j$, $f_i(x) = f_j(x)$). Let $T \subseteq \bigcup_i S_i$ be a subset, and let $x \in S_i$ be an element such that $x \in T$. Then the lifted function $\text{iUnionLift}$ satisfies $\text{iUnionLift}(S, f, hf, T, hT) \langle x, hx \rangle = f_i(x)$, where $hf$ is the proof of pairwise agreement and $hT$ is the proof that $T$ is a subset of the union.

Set.iUnionLift_inclusion theorem

{i : ι} (x : S i) (h : S i ⊆ T) : iUnionLift S f hf T hT (Set.inclusion h x) = f i x

Full source

theorem iUnionLift_inclusion {i : ι} (x : S i) (h : S i ⊆ T) :
    iUnionLift S f hf T hT (Set.inclusion h x) = f i x :=
  iUnionLift_mk x _

Union Lift Preserves Function Values under Inclusion

Informal description

Let $S : \iota \to \text{Set } \alpha$ be an indexed family of sets, and let $f_i : S_i \to \beta$ be a family of functions for each $i \in \iota$ that agree on pairwise intersections (i.e., for any $i, j \in \iota$ and $x \in S_i \cap S_j$, $f_i(x) = f_j(x)$). Let $T \subseteq \bigcup_i S_i$ be a subset, and suppose $S_i \subseteq T$ for some $i \in \iota$. Then for any $x \in S_i$, the lifted function satisfies $\text{iUnionLift}(S, f, T, hT)(\text{inclusion}(h)(x)) = f_i(x)$, where $\text{inclusion}(h)$ is the canonical injection of $S_i$ into $T$.

Set.iUnionLift_of_mem theorem

(x : T) {i : ι} (hx : (x : α) ∈ S i) : iUnionLift S f hf T hT x = f i ⟨x, hx⟩

Full source

theorem iUnionLift_of_mem (x : T) {i : ι} (hx : (x : α) ∈ S i) :
    iUnionLift S f hf T hT x = f i ⟨x, hx⟩ := by obtain ⟨x, hx⟩ := x; exact hf _ _ _ _ _

Value of Union Lift on a Member Set

Informal description

Let $S : \iota \to \text{Set } \alpha$ be an indexed family of sets, and let $f_i : S_i \to \beta$ be a family of functions that agree on pairwise intersections (i.e., for any $i, j \in \iota$ and $x \in S_i \cap S_j$, $f_i(x) = f_j(x)$). Let $T \subseteq \bigcup_i S_i$ and $x \in T$. If $x$ belongs to $S_i$ for some $i \in \iota$, then the lifted function $\text{iUnionLift}$ satisfies $\text{iUnionLift}(S, f, T, hT)(x) = f_i(x)$.

Set.preimage_iUnionLift theorem

 (t : Set β) : iUnionLift S f hf T hT ⁻¹' t = inclusion hT ⁻¹' (⋃ i, inclusion (subset_iUnion S i) '' (f i ⁻¹' t))

Full source

theorem preimage_iUnionLift (t : Set β) :
    iUnionLiftiUnionLift S f hf T hT ⁻¹' t =
      inclusioninclusion hT ⁻¹' (⋃ i, inclusion (subset_iUnion S i) '' (f i ⁻¹' t)) := by
  ext x
  simp only [mem_preimage, mem_iUnion, mem_image]
  constructor
  · rcases mem_iUnion.1 (hT x.prop) with ⟨i, hi⟩
    refine fun h => ⟨i, ⟨x, hi⟩, ?_, rfl⟩
    rwa [iUnionLift_of_mem x hi] at h
  · rintro ⟨i, ⟨y, hi⟩, h, hxy⟩
    obtain rfl : y = x := congr_arg Subtype.val hxy
    rwa [iUnionLift_of_mem x hi]

Preimage Characterization of Union Lift Function

Informal description

Let $S : \iota \to \text{Set } \alpha$ be an indexed family of sets, and let $f_i : S_i \to \beta$ be a family of functions that agree on pairwise intersections. Let $T \subseteq \bigcup_i S_i$ and $hT$ be a proof of this inclusion. For any subset $t \subseteq \beta$, the preimage of $t$ under the lifted function $\text{iUnionLift}(S, f, T, hT)$ is equal to the preimage under the inclusion map $\text{inclusion}(hT)$ of the union over all $i \in \iota$ of the images under $\text{inclusion}(\text{subset\_iUnion } S i)$ of the preimages $f_i^{-1}(t)$. In symbols: $$ (\text{iUnionLift } S f hf T hT)^{-1}(t) = \text{inclusion}(hT)^{-1}\left(\bigcup_i \text{inclusion}(\text{subset\_iUnion } S i) \left(f_i^{-1}(t)\right)\right) $$

Set.iUnionLift_const theorem

 (c : T) (ci : ∀ i, S i) (hci : ∀ i, (ci i : α) = c) (cβ : β) (h : ∀ i, f i (ci i) = cβ) : iUnionLift S f hf T hT c = cβ

Full source

/-- `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 iUnionLift_const (c : T) (ci : ∀ i, S i) (hci : ∀ i, (ci i : α) = c) (cβ : β)
    (h : ∀ i, f i (ci i) = cβ) : iUnionLift S f hf T hT c = cβ := by
  let ⟨i, hi⟩ := Set.mem_iUnion.1 (hT c.prop)
  have : ci i = ⟨c, hi⟩ := Subtype.ext (hci i)
  rw [iUnionLift_of_mem _ hi, ← this, h]

Preservation of Constants under Union Lift

Informal description

Let $S : \iota \to \text{Set } \alpha$ be an indexed family of sets, and let $f_i : S_i \to \beta$ be a family of functions that agree on pairwise intersections. Given a constant element $c \in T \subseteq \bigcup_i S_i$, suppose for each index $i$ there exists an element $c_i \in S_i$ such that $c_i = c$ (as elements of $\alpha$), and a constant $c_\beta \in \beta$ such that $f_i(c_i) = c_\beta$ for all $i$. Then the lifted function satisfies $\text{iUnionLift}(S, f, T, hT)(c) = c_\beta$.

Set.iUnionLift_unary theorem

 (u : T → T) (ui : ∀ i, S i → S i)
  (hui :
    ∀ (i) (x : S i),
      u (Set.inclusion (show S i ⊆ T from hT'.symm ▸ Set.subset_iUnion S i) x) =
        Set.inclusion (show S i ⊆ T from hT'.symm ▸ Set.subset_iUnion S i) (ui i x))
  (uβ : β → β) (h : ∀ (i) (x : S i), f i (ui i x) = uβ (f i x)) (x : T) :
  iUnionLift S f hf T (le_of_eq hT') (u x) = uβ (iUnionLift S f hf T (le_of_eq hT') x)

Full source

/-- `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 iUnionLift_unary (u : T → T) (ui : ∀ i, S i → S i)
    (hui :
      ∀ (i) (x : S i),
        u (Set.inclusion (show S i ⊆ T from hT'.symm ▸ Set.subset_iUnion S i) x) =
          Set.inclusion (show S i ⊆ T from hT'.symm ▸ Set.subset_iUnion S i) (ui i x))
    (uβ : β → β) (h : ∀ (i) (x : S i), f i (ui i x) = uβ (f i x)) (x : T) :
    iUnionLift S f hf T (le_of_eq hT') (u x) = uβ (iUnionLift S f hf T (le_of_eq hT') x) := by
  subst hT'
  obtain ⟨i, hi⟩ := Set.mem_iUnion.1 x.prop
  rw [iUnionLift_of_mem x hi, ← h i]
  have : x = Set.inclusion (Set.subset_iUnion S i) ⟨x, hi⟩ := by
    cases x
    rfl
  conv_lhs => rw [this, hui, iUnionLift_inclusion]

Preservation of Unary Operations under Union Lift

Informal description

Let $S : \iota \to \text{Set } \alpha$ be an indexed family of sets with $T = \bigcup_i S_i$. Given: - A unary operation $u : T \to T$, - For each $i \in \iota$, a unary operation $u_i : S_i \to S_i$ such that $u$ and $u_i$ are compatible via the inclusion maps, - A unary operation $u_\beta : \beta \to \beta$, - For each $i \in \iota$, a function $f_i : S_i \to \beta$ such that $f_i(u_i(x)) = u_\beta(f_i(x))$ for all $x \in S_i$. Then for any $x \in T$, the lifted function satisfies: \[ \text{iUnionLift}(S, f, T)(u(x)) = u_\beta(\text{iUnionLift}(S, f, T)(x)). \]

Set.iUnionLift_binary theorem

 (dir : Directed (· ≤ ·) S) (op : T → T → T) (opi : ∀ i, S i → S i → S i)
  (hopi :
    ∀ i x y,
      Set.inclusion (show S i ⊆ T from hT'.symm ▸ Set.subset_iUnion S i) (opi i x y) =
        op (Set.inclusion (show S i ⊆ T from hT'.symm ▸ Set.subset_iUnion S i) x)
          (Set.inclusion (show S i ⊆ T from hT'.symm ▸ Set.subset_iUnion S i) y))
  (opβ : β → β → β) (h : ∀ (i) (x y : S i), f i (opi i x y) = opβ (f i x) (f i y)) (x y : T) :
  iUnionLift S f hf T (le_of_eq hT') (op x y) =
    opβ (iUnionLift S f hf T (le_of_eq hT') x) (iUnionLift S f hf T (le_of_eq hT') y)

Full source

/-- `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 `*`. -/
theorem iUnionLift_binary (dir : Directed (· ≤ ·) S) (op : T → T → T) (opi : ∀ i, S i → S i → S i)
    (hopi :
      ∀ i x y,
        Set.inclusion (show S i ⊆ T from hT'.symm ▸ Set.subset_iUnion S i) (opi i x y) =
          op (Set.inclusion (show S i ⊆ T from hT'.symm ▸ Set.subset_iUnion S i) x)
            (Set.inclusion (show S i ⊆ T from hT'.symm ▸ Set.subset_iUnion S i) y))
    (opβ : β → β → β) (h : ∀ (i) (x y : S i), f i (opi i x y) = opβ (f i x) (f i y)) (x y : T) :
    iUnionLift S f hf T (le_of_eq hT') (op x y) =
      opβ (iUnionLift S f hf T (le_of_eq hT') x) (iUnionLift S f hf T (le_of_eq hT') y) := by
  subst hT'
  obtain ⟨i, hi⟩ := Set.mem_iUnion.1 x.prop
  obtain ⟨j, hj⟩ := Set.mem_iUnion.1 y.prop
  rcases dir i j with ⟨k, hik, hjk⟩
  rw [iUnionLift_of_mem x (hik hi), iUnionLift_of_mem y (hjk hj), ← h k]
  have hx : x = Set.inclusion (Set.subset_iUnion S k) ⟨x, hik hi⟩ := by
    cases x
    rfl
  have hy : y = Set.inclusion (Set.subset_iUnion S k) ⟨y, hjk hj⟩ := by
    cases y
    rfl
  have hxy : (Set.inclusion (Set.subset_iUnion S k) (opi k ⟨x, hik hi⟩ ⟨y, hjk hj⟩) : α) ∈ S k :=
    (opi k ⟨x, hik hi⟩ ⟨y, hjk hj⟩).prop
  conv_lhs => rw [hx, hy, ← hopi, iUnionLift_of_mem _ hxy]

Preservation of Binary Operations under Union Lift

Informal description

Let $S : \iota \to \text{Set } \alpha$ be a directed family of sets with respect to the subset relation $\subseteq$, and let $T = \bigcup_i S_i$. Suppose we have: - A binary operation $\text{op} : T \to T \to T$, - For each $i \in \iota$, a binary operation $\text{op}_i : S_i \to S_i \to S_i$ such that $\text{op}_i$ is compatible with $\text{op}$ via the inclusion maps, - A binary operation $\text{op}_\beta : \beta \to \beta \to \beta$, - For each $i \in \iota$, a function $f_i : S_i \to \beta$ such that $f_i(\text{op}_i(x, y)) = \text{op}_\beta(f_i(x), f_i(y))$ for all $x, y \in S_i$. Then for any $x, y \in T$, the lifted function $\text{iUnionLift}$ satisfies: \[ \text{iUnionLift}(S, f, T)(\text{op}(x, y)) = \text{op}_\beta(\text{iUnionLift}(S, f, T)(x), \text{iUnionLift}(S, f, T)(y)). \]

Set.liftCover definition

 (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 : iUnion S = univ) (a : α) : β

Full source

/-- Glue together functions defined on each of a collection `S` of sets that cover a type. See
also `Set.iUnionLift`. -/
noncomputable def liftCover (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 : iUnion S = univ) (a : α) : β :=
  iUnionLift S f hf univ hS.symm.subset ⟨a, trivial⟩

Function lifting over a cover of sets

Informal description

Given an indexed family of sets $ S : \iota \to \text{Set } \alpha $ covering the entire type $\alpha$ (i.e., $\bigcup_i S_i = \alpha$), and a family of functions $ f_i : S_i \to \beta $ that agree on pairwise intersections (i.e., for any $ i, j \in \iota $ and $ x \in S_i \cap S_j $, $ f_i(x) = f_j(x) $), the function `Set.liftCover` constructs a function from $\alpha$ to $\beta$ by lifting the functions $ f_i $ to the entire type $\alpha$. Specifically, for any $ a \in \alpha $, it selects an index $ i $ such that $ a \in S_i $ and returns $ f_i(a) $.

Set.liftCover_coe theorem

{i : ι} (x : S i) : liftCover S f hf hS x = f i x

Full source

@[simp]
theorem liftCover_coe {i : ι} (x : S i) : liftCover S f hf hS x = f i x :=
  iUnionLift_mk x _

Value of Lift Cover on Elements from Component Sets

Informal description

Let $S : \iota \to \text{Set } \alpha$ be an indexed family of sets covering $\alpha$ (i.e., $\bigcup_i S_i = \alpha$), and let $f_i : S_i \to \beta$ be a family of functions that agree on pairwise intersections. For any index $i$ and element $x \in S_i$, the lifted function $\text{liftCover}$ satisfies $\text{liftCover}(S, f, hf, hS)(x) = f_i(x)$, where $hf$ is the proof of pairwise agreement and $hS$ is the proof that the union covers $\alpha$.

Set.liftCover_of_mem theorem

{i : ι} {x : α} (hx : (x : α) ∈ S i) : liftCover S f hf hS x = f i ⟨x, hx⟩

Full source

theorem liftCover_of_mem {i : ι} {x : α} (hx : (x : α) ∈ S i) :
    liftCover S f hf hS x = f i ⟨x, hx⟩ :=
  iUnionLift_of_mem (⟨x, trivial⟩ : {_z // True}) hx

Value of Lift Cover on a Member Set

Informal description

Let $S : \iota \to \text{Set } \alpha$ be an indexed family of sets covering $\alpha$ (i.e., $\bigcup_i S_i = \alpha$), and let $f_i : S_i \to \beta$ be a family of functions that agree on pairwise intersections. For any $x \in \alpha$ and $i \in \iota$ such that $x \in S_i$, the lifted function $\text{liftCover}$ satisfies $\text{liftCover}(S, f, hf, hS)(x) = f_i(x)$.

Set.preimage_liftCover theorem

(t : Set β) : liftCover S f hf hS ⁻¹' t = ⋃ i, (↑) '' (f i ⁻¹' t)

Full source

theorem preimage_liftCover (t : Set β) : liftCoverliftCover S f hf hS ⁻¹' t = ⋃ i, (↑) '' (f i ⁻¹' t) := by
  change (iUnionLift S f hf univ hS.symm.subset ∘ fun a => ⟨a, mem_univ a⟩) ⁻¹' t = _
  rw [preimage_comp, preimage_iUnionLift]
  ext; simp

Preimage Characterization of Lift Cover Function

Informal description

Let $S : \iota \to \text{Set } \alpha$ be an indexed family of sets covering $\alpha$ (i.e., $\bigcup_i S_i = \alpha$), and let $f_i : S_i \to \beta$ be a family of functions that agree on pairwise intersections. For any subset $t \subseteq \beta$, the preimage of $t$ under the lifted function $\text{liftCover}(S, f, hf, hS)$ is equal to the union over all $i \in \iota$ of the images of the preimages $f_i^{-1}(t)$ under the canonical inclusion map from $S_i$ to $\alpha$. In symbols: $$ (\text{liftCover } S f hf hS)^{-1}(t) = \bigcup_{i \in \iota} \{x \in \alpha \mid \exists y \in S_i, y = x \text{ and } f_i(y) \in t\} $$