lift — Mathlib

English

For an invariant map f with the same invariance hypothesis h, the composition lift ρ f h with mk ρ equals f.

Русский

При инвариантном отображении f выполнено, что lift ρ f h прямо композится с mk ρ до f.

LaTeX

$$$\mathrm{lift}_\rho f h \circ mk_\rho = f$$$

Lean4

/-- A `G`-invariant linear map induces a linear map out of the coinvariants of a
`G`-representation. -/
def lift (f : V →ₗ[k] W) (h : ∀ (x : G), f ∘ₗ ρ x = f) : ρ.Coinvariants →ₗ[k] W :=
  Submodule.liftQ _ f <|
    Submodule.span_le.2 fun x ⟨⟨g, y⟩, hy⟩ => by
      simpa only [← hy, SetLike.mem_coe, LinearMap.mem_ker, map_sub, sub_eq_zero, LinearMap.coe_comp,
        Function.comp_apply] using LinearMap.ext_iff.1 (h g) y

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