quotOfListConsSMulTopEquivQuotSMulTopInner_naturality

English

Naturality of the inner quotient equivalence with respect to f (duplicate): equality of two ways of composing maps.

Русский

Естественность внутреннего эквивалентного отображения относительно f (повтор): равенство двух способов композиции отображений.

LaTeX

$$Same as 184123 (duplicate nat).$$

Lean4

theorem quotOfListConsSMulTopEquivQuotSMulTopInner_naturality (f : M →ₗ[R] M₂) :
    (quotOfListConsSMulTopEquivQuotSMulTopInner M₂ r rs).toLinearMap ∘ₗ
        mapQ _ _ _ (smul_top_le_comap_smul_top (Ideal.ofList (r :: rs)) f) =
      mapQ _ _ _ (smul_top_le_comap_smul_top _ (QuotSMulTop.map r f)) ∘ₗ
        (quotOfListConsSMulTopEquivQuotSMulTopInner M r rs).toLinearMap :=
  quot_hom_ext _ _ _ fun _ => rfl

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