equivComp — Mathlib

English

The composition of an isomorphism between equivalent extensions with a section yields a section of the target extension.

Русский

Сложение изоморфизма между эквивалентными расширениями и секции даёт секцию целевого расширения.

LaTeX

$$$ \\text{equivComp} : S'\\Section \\to S.Section \\text{ with } (toFun := \\text{equiv} \\circ \\sigma) $$$

Lean4

/-- The composition of an isomorphism between equivalent group extensions and a section -/
@[to_additive (attr := simps!) /--
    The composition of an isomorphism between equivalent additive group extensions and a section -/
    ]
def equivComp : S'.Section where
  toFun := equiv ∘ σ
  rightInverse_rightHom g := by rw [Function.comp_apply, equiv.rightHom_map, rightHom_section]

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