noncommPiCoprod_mrange — Mathlib

English

The coproduct composed with inl and inr gives identity on M × N.

Русский

Копродукт после вставок inl и inr даёт тождество на M × N.

LaTeX

$$$ (\\mathrm{inl} M N).noncommCoprod (\\mathrm{inr} M N) comm = \\mathrm{id}_{M \\times N}.$$$

Lean4

@[to_additive]
theorem noncommPiCoprod_mrange : MonoidHom.mrange (noncommPiCoprod ϕ hcomm) = ⨆ i : ι, MonoidHom.mrange (ϕ i) :=
  by
  letI := Classical.decEq ι
  apply le_antisymm
  · rintro x ⟨f, rfl⟩
    refine Submonoid.noncommProd_mem _ _ _ (fun _ _ _ _ h => hcomm h _ _) (fun i _ => ?_)
    apply Submonoid.mem_sSup_of_mem
    · use i
    simp
  · refine iSup_le ?_
    rintro i x ⟨y, rfl⟩
    exact ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩

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