English
On an element x of S_i, liftCover S f hf hS x equals f_i x after identifying x with its image in α.
Русский
Для элемента x из S_i liftCover S f hf hS x равен f_i x после тождества x с образом в α.
LaTeX
$$$\\forall i, \\forall x\\in S_i:\\ \\text{liftCover}(S,f,hf,hS)(x) = f_i(x).$$$
Lean4
/-- `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]
