English
If on each S_i you have a specified element c_i representing the same element c ∈ T and all f_i(c_i) equal a fixed cβ, then the glued value on c equals cβ.
Русский
Если на каждом S_i есть соответствующий элемент c_i, представляющий одно и то же c ∈ T, и все f_i(c_i) равны фиксированному cβ, то склеенное значение на c равно cβ.
LaTeX
$$$\\text{If } c\\in T,\\; \\exists c_i\\in S_i\\text{ with } (c_i)\\text{ representing } c\\text{ and } f_i(c_i)=c_β\\ \forall i, \\ f_i(c_i)=c_β \\Rightarrow iUnionLift S f hf T hT c = c_β.$$$
Lean4
/-- `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]
