comap_codRestrict — Mathlib

English

The symm of orderIsoMapComap satisfies (orderIsoMapComap e).symm p = map e.symm p.

Русский

Обратное отображение orderIsoMapComap e удовлетворяет (orderIsoMapComap e).symm p = map e.symm p.

LaTeX

$$$ (orderIsoMapComap e).symm p = map e.symm p $$$

Lean4

theorem comap_codRestrict (p : Submodule R M) (f : M₂ →ₛₗ[σ₂₁] M) (hf p') :
    Submodule.comap (codRestrict p f hf) p' = Submodule.comap f (map p.subtype p') :=
  Submodule.ext fun x => ⟨fun h => ⟨⟨_, hf x⟩, h, rfl⟩, by rintro ⟨⟨_, _⟩, h, ⟨⟩⟩; exact h⟩

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