English
LiftCover is the glued function on α obtained by gluing the family {f_i} along the cover {S_i}; it coincides with iUnionLift on the case T = univ.
Русский
LiftCover — это склеенная функция на α, полученная склейкой по покрытию {S_i}; она совпадает с iUnionLift в случае T = univ.
LaTeX
$$$\text{liftCover}(S,f,hf,hS) : α \to β\quad\text{defined by}\quad (a) = iUnionLift S f hf\; univ\; hS^{-1}.\{\text{вклад}\langle a, \text{trivial}\rangle\}.$$$
Lean4
/-- `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]
