full_res — Mathlib

English

The restriction functor is full when the homomorphism f is surjective.

Русский

Ограничение полно, если гомоморфизм f сюръективен.

LaTeX

$$full_res (f_surj : Function.Surjective f) : (res V f).Full$$

Lean4

/-- The functor from `Action V H` to `Action V G` induced by a morphism `f : G → H` is full
if `f` is surjective. -/
theorem full_res (f_surj : Function.Surjective f) : (res V f).Full where
  map_surjective {X} {Y}
    g := by
    use ⟨g.hom, fun h ↦ ?_⟩
    · ext
      simp
    · obtain ⟨a, rfl⟩ := f_surj h
      have : X.ρ (f a) = ((res V f).obj X).ρ a := rfl
      rw [this, g.comm a]
      simp

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