Set.iUnionLift_binary
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 ⟨x, hxi⟩ = f j ⟨x, hxj⟩} {T : Set α}
{hT : T ⊆ Set.iUnion S} (hT' : T = Set.iUnion S),
Directed (fun x x_1 => x ≤ x_1) S →
∀ (op : ↑T → ↑T → ↑T) (opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)),
(∀ (i : ι) (x y : ↑(S i)), Set.inclusion ⋯ (opi i x y) = op (Set.inclusion ⋯ x) (Set.inclusion ⋯ y)) →
∀ (opβ : β → β → β),
(∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)) →
∀ (x 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)
The `iUnionLift_binary` theorem in Lean 4 is a valuable tool for proving that the `iUnionLift` function maintains the structure of algebraic operations when applied to the union of algebraic subobjects. This theorem takes a collection of set-indexed functions `f` from elements of the subobjects `S i` to some type `β`, an operation `op` on a set `T` that is a subset of the union of `S i`, and a corresponding operation `opi` on each `S i`. Under the conditions that these operations adhere to the inclusion function and that `f` homomorphically relates `opi` and an operation `opβ` on `β`, the theorem establishes that `iUnionLift`, when applied to `op` on `T`, equals `opβ` applied to `iUnionLift` on the corresponding elements of `T`. This is useful for demonstrating, for instance, that the lift of a collection of group homomorphisms on a union of subgroups preserves the group operation.
More concisely: Given a collection of set-indexed homomorphisms `f` from subobjects `S i` to a type `β`, an operation `op` on a set `T` that is a subset of the union of `S i`, and corresponding homomorphic operations `opi` on each `S i`, the `iUnionLift` of `op` on `T` equals the application of `opβ` to `iUnionLift` on the corresponding elements of `T`, provided `opi` and `opβ` are related by `f`.
|
Set.iUnionLift_const
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 ⟨x, hxi⟩ = f j ⟨x, hxj⟩} {T : Set α}
{hT : T ⊆ Set.iUnion S} (c : ↑T) (ci : (i : ι) → ↑(S i)),
(∀ (i : ι), ↑(ci i) = ↑c) → ∀ (cβ : β), (∀ (i : ι), f i (ci i) = cβ) → Set.iUnionLift S f hf T hT c = cβ
The theorem `Set.iUnionLift_const` states that for any type `α`, any type `ι` that indexes a family of sets, any type `β`, any family of sets `S`, any function `f` defined on each component of the family of sets, and any set `T` that is a subset of the union of the family of sets, if we have a constant `c` in `T` and a function `ci` that maps each index to an element in the corresponding set such that each element equals `c`, and if for each index `i`, the function `f` applied to the element `ci i` equals a constant `cβ`, then applying the function `Set.iUnionLift` to `S`, `f`, `T`, and `c` yields `cβ`. This theorem can be useful when proving that `Set.iUnionLift` preserves algebraic structure 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 the identity element `1`.
More concisely: Given a family of sets `S` indexed by `ι`, a constant `c` in the union of `S`, functions `ci : ι -> S i` with `ci i = c` for all `i`, `f : ∀ i, S i -> β`, and `cβ` such that `f (ci i) = cβ` for all `i`, `Set.iUnionLift S f T c = cβ` whenever `T` is a subset of the union of `S`.
|
Set.iUnionLift_unary
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 ⟨x, hxi⟩ = f j ⟨x, hxj⟩} {T : Set α}
{hT : T ⊆ Set.iUnion S} (hT' : T = Set.iUnion S) (u : ↑T → ↑T) (ui : (i : ι) → ↑(S i) → ↑(S i)),
(∀ (i : ι) (x : ↑(S i)), u (Set.inclusion ⋯ x) = Set.inclusion ⋯ (ui i x)) →
∀ (uβ : β → β),
(∀ (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)
The theorem `Set.iUnionLift_unary` helps to prove that the function `iUnionLift` acts as a homomorphism when it is defined on the union of algebraic subobjects. More specifically, consider a collection of sets, each one indexed by an element from some other set. Suppose we have defined a function for each of these sets, and these functions agree on intersections. If we define a function, `u`, on the union of these sets, and analogous functions, `ui`, on each individual set, such that the function on the union respects the functions on the individual sets, then a function, `uβ`, on the codomain `β`, if it commutes with `f` and `ui`, will also commute with the lift of `f` and `u`. This property can be used, for example, to show that the lift of a collection of linear maps on the union of submodules preserves scalar multiplication.
More concisely: If `f` commutes with `ui` for all subobjects `i` of a set and `u` is a function that respects `ui` on their union, then `f` commutes with the lifted function `uβ` on the codomain.
|
Set.iUnionLift.proof_1
theorem Set.iUnionLift.proof_1 :
∀ {α : Type u_2} {ι : Sort u_1} (S : ι → Set α), ∀ T ⊆ Set.iUnion S, ∀ (x : ↑T), ∃ i, ↑x ∈ S i
The theorem `Set.iUnionLift.proof_1` states that for any type `α`, any sort `ι`, and any family of sets `S` indexed by `ι`, if a set `T` is a subset of the indexed union of the family `S`, then for every element `x` in `T`, there exists an index `i` such that `x` is in the set `S i`. In other words, every element of a subset of an indexed union of sets comes from at least one of the sets in the union.
More concisely: If `T` is a subset of the indexed union of a family `S` of sets indexed by `ι`, then for every `x` in `T`, there exists an index `i` such that `x` is in `S i`.
|