Documentation

LeanPool.RegtsSevenster.RS.Classical.Deligne.SuperModIso

Recognising isomorphisms of super modules #

A morphism of super modules whose two components are bijective is an isomorphism: the componentwise inverses are again ℂ-linear and again commute with the four actions, because the actions on the source are determined by those on the target.

source
noncomputable def RS.SuperCommAlgebra.Mod.isoOfComponents {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) (he : Function.Bijective ⇑f.evenMap) (ho : Function.Bijective ⇑f.oddMap) :
M ≅ N

A degreewise bijective morphism of super modules is an isomorphism.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem RS.SuperCommAlgebra.Mod.isIso_of_components {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) (he : Function.Bijective ⇑f.evenMap) (ho : Function.Bijective ⇑f.oddMap) :
    CategoryTheory.IsIso f

    A degreewise bijective morphism of super modules is an isomorphism, as an instance-friendly statement.