coindVEquiv — Mathlib

English

There exists an instance showing that the coinduction functor preserves epimorphisms along a subgroup subtype, i.e., surjective maps remain surjective after coinduction.

Русский

Существование инстанса, доказывающего, что коиндукционный функтор сохраняет эпиморфизмы вдоль подгруппы.

LaTeX

$$$\text{coindFunctor}_k S.\text{perse} ext{rves epi}$$$

Lean4

/-- If `φ : G →* H` and `A : Rep k G` then the `k`-submodule of functions `f : H → A`
such that for all `g : G`, `h : H`, `f (φ g * h) = A.ρ g (f h)`, is `k`-linearly equivalent
to the `G`-representation morphisms `k[H] ⟶ A`.
-/
@[simps]
noncomputable def coindVEquiv : A.ρ.coindV φ ≃ₗ[k] ((Action.res _ φ).obj (leftRegular k H) ⟶ A)
    where
  toFun
    f :=
    { hom := ModuleCat.ofHom <| linearCombination _ f.1
      comm g := ModuleCat.hom_ext <| lhom_ext' fun _ => LinearMap.ext_ring <| by simp [ModuleCat.endRingEquiv, f.2 g] }
  map_add' _ _ := coind'_ext φ fun _ => by simp
  map_smul' _ _ := coind'_ext φ fun _ => by simp
  invFun
    f :=
    { val h := f.hom (single h 1)
      property g h := by have := (hom_comm_apply f g (single h 1)).symm; simp_all [Rep.res_obj_ρ φ] }
  left_inv x := by simp
  right_inv x := coind'_ext φ fun _ => by simp

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