English
The coweightEquiv associated to an equivalence e is defined by LinearEquiv.ofBijective using the bijection e.bijective_coweightMap.
Русский
Ковейтовое эквивалентность к эквивалентности e определяется через линейное эквивалентность LinearEquiv.ofBijective, используя биективное отображение ковейтов.
LaTeX
$$$\mathrm{coweightEquiv}(P,Q,e) = \mathrm{LinearEquiv.ofBijective} (\_, e.bijective\_coweightMap)$$$
Lean4
/-- Composition of equivalences -/
@[simps!]
def comp {ι₁ M₁ N₁ ι₂ M₂ N₂ : Type*} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁] [Module R N₁] [AddCommGroup M₂]
[Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁}
{P₂ : RootPairing ι₂ R M₂ N₂} (g : RootPairing.Equiv P₁ P₂) (f : RootPairing.Equiv P P₁) : RootPairing.Equiv P P₂ :=
{
Hom.comp g.toHom
f.toHom with
bijective_weightMap := by
simp only [Hom.comp, LinearMap.coe_comp]
exact Bijective.comp g.bijective_weightMap f.bijective_weightMap
bijective_coweightMap := by
simp only [Hom.comp, LinearMap.coe_comp]
exact Bijective.comp f.bijective_coweightMap g.bijective_coweightMap }
