homRestrict_hasLift — Mathlib

English

Let e, φ, hφ be as above. For i′, i with hi: e.f i = i′, the morphism (e.liftExtend φ hφ).f i′ is mono iff φ.f i is mono.

Русский

Пусть e, φ, hφ как выше. Для i′, i с hi: e.f i = i′, отображение (e.liftExtend φ hφ).f i′ монотонно эквивалентно φ.f i.

LaTeX

$$$$ \forall i\, \forall i'\, (hi : e.f i = i'):\quad Mono\big((e.liftExtend φ hφ).f i'\big) \iff Mono(φ.f i) $$$$

Lean4

theorem homRestrict_hasLift (ψ : K ⟶ L.extend e) : e.HasLift (e.homRestrict ψ) :=
  by
  intro j hj i' hij'
  have : (L.extend e).d i' (e.f j) = 0 := by apply (L.isZero_extend_X e i' (hj.notMem hij')).eq_of_src
  dsimp [homRestrict]
  rw [homRestrict.f_eq ψ rfl, restrictionXIso, eqToIso_refl, Iso.refl_hom, id_comp, ← ψ.comm_assoc, this, zero_comp,
    comp_zero]

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