liftExtend_homRestrict — Mathlib

English

For ψ: K ⟶ L.extend e, the liftExtend of e.homRestrict ψ with e.homRestrict_hasLift ψ equals ψ.

Русский

Для ψ: K ⟶ L.extend e подъём расширения e.homRestrict ψ с e.homRestrict_hasLift ψ равен ψ.

LaTeX

$$$$ e.liftExtend \, (e.homRestrict ψ) \, (e.homRestrict_hasLift ψ) = ψ $$$$

Lean4

@[simp]
theorem liftExtend_homRestrict (ψ : K ⟶ L.extend e) : e.liftExtend (e.homRestrict ψ) (e.homRestrict_hasLift ψ) = ψ :=
  by
  ext i'
  by_cases hi' : ∃ i, e.f i = i'
  · obtain ⟨i, rfl⟩ := hi'
    simp [e.homRestrict_f _ rfl, e.liftExtend_f _ _ rfl]
  · apply (L.isZero_extend_X e i' (by simpa using hi')).eq_of_tgt

Похожие утверждения