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 #
Set.unionᵢLift
- Given a Union of setsunionᵢ 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 ofSet.unionᵢLift
for the special case that the sets cover the entire type.
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
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.
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
.
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.
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 *
.
Glue together functions defined on each of a collection S
of sets that cover a type. See
also Set.unionᵢLift
.
Equations
- Set.liftCover S f hf hS a = Set.unionᵢLift S f hf Set.univ (_ : Set.univ ⊆ Set.unionᵢ S) { val := a, property := trivial }