surjective_compr₂ₛₗ_of_equiv

English

A variant showing the bijectivity of f.compr₂ g when f is bijective and g is an equivalence.

Русский

Вариант показывает биективность f.compr₂ g при f биективной и g эквивалентности.

LaTeX

$$$\text{Bijective}(f) \Rightarrow \text{Bijective}(f.compr₂ g.toLinearMap).$$$

Lean4

/-- A version of `Function.Surjective.comp` for composition of a bilinear map with a linear map. -/
theorem surjective_compr₂ₛₗ_of_equiv [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P)
    (g : P ≃ₛₗ[σ₃₄] Q) (hf : Surjective f) : Surjective (f.compr₂ₛₗ g.toLinearMap) :=
  surjective_compr₂ₛₗ_of_exists_rightInverse f g.toLinearMap hf ⟨g.symm, by simp⟩

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