lift_surjective_iff — Mathlib

English

Characterization of lift surjectivity via a lifting condition on g.

Русский

Характеризация сюръективности лифта через условие подъёма на g.

LaTeX

$$$ \\operatorname{Surjective}(f.lift\\; hg) \\iff \\forall v \\in P, \\ exists\\ x=(x_1,x_2)\\in M\\times S\\ such\ that\\ v\\cdot g(x_2)=g(x_1) $$$

Lean4

@[to_additive]
theorem lift_surjective_iff : Function.Surjective (f.lift hg) ↔ ∀ v : P, ∃ x : M × S, v * g x.2 = g x.1 :=
  by
  constructor
  · intro H v
    obtain ⟨z, hz⟩ := H v
    obtain ⟨x, hx⟩ := f.surj z
    use x
    rw [← hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2), ← MonoidHom.restrict_apply,
      IsUnit.mul_liftRight_inv (g.restrict S) hg, mul_one]
  · intro H v
    obtain ⟨x, hx⟩ := H v
    use f.mk' x.1 x.2
    rw [lift_mk', mul_inv_left hg, mul_comm, ← hx]

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