tensorProductFanIso — Mathlib

English

There is a canonical isomorphism between tensorProductFan S P and tensorProductFan' S P when ι is finite, compatible with the projections.

Русский

Существует каноническое изоморфизм между tensorProductFan S P и tensorProductFan' S P, если ι конечен, совместимый с проекциями.

LaTeX

$$$\\text{tensorProductFanIso} : (\\text{tensorProductFan } S P) \\cong (\\text{tensorProductFan'} S P)$$$

Lean4

/-- The two fans on `i ↦ S ⊗[R] P i` agree if `ι` is finite. -/
def tensorProductFanIso [Fintype ι] [DecidableEq ι] : tensorProductFan S P ≅ tensorProductFan' S P :=
  Fan.ext (Algebra.TensorProduct.piRight R S _ _).toUnder <| fun i ↦
    by
    dsimp only [tensorProductFan, Fan.mk_pt, fan_mk_proj, tensorProductFan']
    apply CommRingCat.mkUnder_ext
    intro c
    induction c
    · simp only [map_zero, Under.comp_right]
    ·
      simp only [AlgHom.toUnder_right, Algebra.TensorProduct.map_tmul, AlgHom.coe_id, id_eq, Pi.evalAlgHom_apply,
        Under.comp_right, comp_apply, AlgEquiv.toUnder_hom_right_apply, Algebra.TensorProduct.piRight_tmul]
    · simp_all

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