Documentation

LeanPool.RegtsSevenster.RS.Classical.Deligne.SuperModAbelian

Super modules form an abelian category #

A module over a super-commutative ℂ-algebra S is a pair of ℂ-modules carrying four bilinear action blocks, and a morphism is a pair of ℂ-linear maps intertwining those blocks. Every construction needed for abelianness is therefore performed degreewise in Module ℂ:

the kernel is the pair of kernels of the two components, and the four blocks restrict to it;
the cokernel is the pair of quotients by the two ranges, and the four blocks descend to them;
a morphism is a monomorphism exactly when both of its components are injective, and an epimorphism exactly when both are surjective — the forward directions are read off the kernel and the cokernel respectively;
a monomorphism is the kernel of its cokernel and an epimorphism is the cokernel of its kernel, because a degreewise factorisation through an injective (respectively surjective) component again intertwines the four blocks.

The route taken to CategoryTheory.Abelian is therefore the normality route: the two normality instances, together with the finite products of RS.Classical.Deligne.SuperModBiprod and the kernels and cokernels built here.

Two small pieces of linear algebra carry all of the graded bookkeeping. RS.SuperCommAlgebra.Mod.actRestrict restricts a bilinear action block to a pair of submodules stable under it, and RS.SuperCommAlgebra.Mod.actQuot descends one to a pair of quotients; the ten axioms of a super module are pointwise identities, so each survives verbatim in a submodule and in a quotient.

Restricting and descending an action block #

def RS.SuperCommAlgebra.Mod.actRestrict {A : Type u_1} {E : Type u_2} {F : Type u_3} [AddCommGroup A] [Module ℂ A] [AddCommGroup E] [Module ℂ E] [AddCommGroup F] [Module ℂ F] (φ : A →ₗ[ℂ ] E →ₗ[ℂ ] F) {p : Submodule ℂ E} {q : Submodule ℂ F} (h : ∀ (a : A), ∀ e ∈ p, (φ a) e ∈ q) :

A →ₗ[ℂ ] ↥p →ₗ[ℂ ] ↥q

The restriction of an action block to a pair of submodules carried into one another by it.

Equations

RS.SuperCommAlgebra.Mod.actRestrict φ h = { toFun := fun (a : A) => LinearMap.codRestrict q (φ a ∘ₗ p.subtype) ⋯, map_add' := ⋯, map_smul' := ⋯ }

Instances For

@[simp]

theorem RS.SuperCommAlgebra.Mod.actRestrict_coe {A : Type u_1} {E : Type u_2} {F : Type u_3} [AddCommGroup A] [Module ℂ A] [AddCommGroup E] [Module ℂ E] [AddCommGroup F] [Module ℂ F] (φ : A →ₗ[ℂ ] E →ₗ[ℂ ] F) {p : Submodule ℂ E} {q : Submodule ℂ F} (h : ∀ (a : A), ∀ e ∈ p, (φ a) e ∈ q) (a : A) (e : ↥p) :

↑(((actRestrict φ h) a) e) = (φ a) ↑e

def RS.SuperCommAlgebra.Mod.actQuot {A : Type u_1} {E : Type u_2} {F : Type u_3} [AddCommGroup A] [Module ℂ A] [AddCommGroup E] [Module ℂ E] [AddCommGroup F] [Module ℂ F] (φ : A →ₗ[ℂ ] E →ₗ[ℂ ] F) {p : Submodule ℂ E} {q : Submodule ℂ F} (h : ∀ (a : A), ∀ e ∈ p, (φ a) e ∈ q) :

A →ₗ[ℂ ] E ⧸ p →ₗ[ℂ ] F ⧸ q

The descent of an action block to a pair of quotients, the first by a submodule carried by the block into the second.

Equations

RS.SuperCommAlgebra.Mod.actQuot φ h = (p.liftQ (φ.compr₂ q.mkQ).flip ⋯).flip

Instances For

@[simp]

theorem RS.SuperCommAlgebra.Mod.actQuot_mk {A : Type u_1} {E : Type u_2} {F : Type u_3} [AddCommGroup A] [Module ℂ A] [AddCommGroup E] [Module ℂ E] [AddCommGroup F] [Module ℂ F] (φ : A →ₗ[ℂ ] E →ₗ[ℂ ] F) {p : Submodule ℂ E} {q : Submodule ℂ F} (h : ∀ (a : A), ∀ e ∈ p, (φ a) e ∈ q) (a : A) (e : E) :

((actQuot φ h) a) (Submodule.Quotient.mk e) = Submodule.Quotient.mk ((φ a) e)

theorem RS.SuperCommAlgebra.Mod.quotMk_congr {F : Type u_3} [AddCommGroup F] [Module ℂ F] {q : Submodule ℂ F} {a b : F} (h : a = b) :

Submodule.Quotient.mk a = Submodule.Quotient.mk b

Congruence for the class map of a quotient module.

Degreewise factorisation #

noncomputable def RS.SuperCommAlgebra.Mod.preimageMap {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommGroup E] [Module ℂ E] [AddCommGroup F] [Module ℂ F] [AddCommGroup G] [Module ℂ G] (g : E →ₗ[ℂ ] G) (φ : F →ₗ[ℂ ] G) (hφ : Function.Injective ⇑φ) (h : ∀ (e : E), g e ∈ φ.range) :

E →ₗ[ℂ ] F

The factorisation of a linear map through an injective one whose range contains its values.

Equations

RS.SuperCommAlgebra.Mod.preimageMap g φ hφ h = ↑(LinearEquiv.ofInjective φ hφ).symm ∘ₗ LinearMap.codRestrict φ.range g h

Instances For

@[simp]

theorem RS.SuperCommAlgebra.Mod.preimageMap_spec {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommGroup E] [Module ℂ E] [AddCommGroup F] [Module ℂ F] [AddCommGroup G] [Module ℂ G] (g : E →ₗ[ℂ ] G) (φ : F →ₗ[ℂ ] G) (hφ : Function.Injective ⇑φ) (h : ∀ (e : E), g e ∈ φ.range) (e : E) :

φ ((preimageMap g φ hφ h) e) = g e

theorem RS.SuperCommAlgebra.Mod.ker_le_ker {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommGroup E] [Module ℂ E] [AddCommGroup F] [Module ℂ F] [AddCommGroup G] [Module ℂ G] (g : E →ₗ[ℂ ] G) (φ : E →ₗ[ℂ ] F) (h : ∀ (e : E), φ e = 0 → g e = 0) :

φ.ker ≤ g.ker

A linear map annihilating the kernel of another has a larger kernel.

noncomputable def RS.SuperCommAlgebra.Mod.quotientMap {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommGroup E] [Module ℂ E] [AddCommGroup F] [Module ℂ F] [AddCommGroup G] [Module ℂ G] (g : E →ₗ[ℂ ] G) (φ : E →ₗ[ℂ ] F) (hφ : Function.Surjective ⇑φ) (h : ∀ (e : E), φ e = 0 → g e = 0) :

F →ₗ[ℂ ] G

The factorisation of a linear map through a surjective one whose kernel it annihilates.

Equations

RS.SuperCommAlgebra.Mod.quotientMap g φ hφ h = φ.ker.liftQ g ⋯ ∘ₗ ↑(φ.quotKerEquivOfSurjective hφ).symm

Instances For

@[simp]

theorem RS.SuperCommAlgebra.Mod.quotientMap_spec {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommGroup E] [Module ℂ E] [AddCommGroup F] [Module ℂ F] [AddCommGroup G] [Module ℂ G] (g : E →ₗ[ℂ ] G) (φ : E →ₗ[ℂ ] F) (hφ : Function.Surjective ⇑φ) (h : ∀ (e : E), φ e = 0 → g e = 0) (e : E) :

(quotientMap g φ hφ h) (φ e) = g e

Degreewise criteria for monomorphisms and epimorphisms #

theorem RS.SuperCommAlgebra.Mod.mono_of_injective {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) (he : Function.Injective ⇑f.evenMap) (ho : Function.Injective ⇑f.oddMap) :

CategoryTheory.Mono f

A degreewise injective morphism of super modules is a monomorphism.

theorem RS.SuperCommAlgebra.Mod.epi_of_surjective {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) (he : Function.Surjective ⇑f.evenMap) (ho : Function.Surjective ⇑f.oddMap) :

CategoryTheory.Epi f

A degreewise surjective morphism of super modules is an epimorphism.

Kernels #

theorem RS.SuperCommAlgebra.Mod.actEE_mem_ker {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) (x : S.even) (m : M.even) (hm : m ∈ f.evenMap.ker) :

(M.actEE x) m ∈ f.evenMap.ker

theorem RS.SuperCommAlgebra.Mod.actEO_mem_ker {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) (x : S.even) (m : M.odd) (hm : m ∈ f.oddMap.ker) :

(M.actEO x) m ∈ f.oddMap.ker

theorem RS.SuperCommAlgebra.Mod.actOE_mem_ker {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) (v : S.odd) (m : M.even) (hm : m ∈ f.evenMap.ker) :

(M.actOE v) m ∈ f.oddMap.ker

theorem RS.SuperCommAlgebra.Mod.actOO_mem_ker {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) (v : S.odd) (m : M.odd) (hm : m ∈ f.oddMap.ker) :

(M.actOO v) m ∈ f.evenMap.ker

def RS.SuperCommAlgebra.Mod.kerMod {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) :

The kernel of a morphism of super modules: the kernels of the two components, with the four action blocks restricted.

Equations

One or more equations did not get rendered due to their size.

Instances For

def RS.SuperCommAlgebra.Mod.kerIncl {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) :

The inclusion of the kernel of a morphism of super modules.

Equations

RS.SuperCommAlgebra.Mod.kerIncl f = { evenMap := f.evenMap.ker.subtype, oddMap := f.oddMap.ker.subtype, map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ }

Instances For

theorem RS.SuperCommAlgebra.Mod.kerIncl_comp {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) :

CategoryTheory.CategoryStruct.comp (kerIncl f) f = 0

theorem RS.SuperCommAlgebra.Mod.mono_kerIncl {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) :

CategoryTheory.Mono (kerIncl f)

The inclusion of the kernel is a monomorphism.

def RS.SuperCommAlgebra.Mod.kerLift {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) {W : S.Mod} (k : W ⟶ M) (hk : CategoryTheory.CategoryStruct.comp k f = 0) :

The lift of a morphism annihilated by f through the inclusion of the kernel.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem RS.SuperCommAlgebra.Mod.kerLift_comp {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) {W : S.Mod} (k : W ⟶ M) (hk : CategoryTheory.CategoryStruct.comp k f = 0) :

CategoryTheory.CategoryStruct.comp (kerLift f k hk) (kerIncl f) = k

def RS.SuperCommAlgebra.Mod.kernelFork {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) :

CategoryTheory.Limits.KernelFork f

The kernel fork of a morphism of super modules.

Equations

RS.SuperCommAlgebra.Mod.kernelFork f = CategoryTheory.Limits.KernelFork.ofι (RS.SuperCommAlgebra.Mod.kerIncl f) ⋯

Instances For

def RS.SuperCommAlgebra.Mod.kernelForkIsLimit {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) :

CategoryTheory.Limits.IsLimit (kernelFork f)

The kernel fork is limiting.

Equations

One or more equations did not get rendered due to their size.

Instances For

instance RS.SuperCommAlgebra.Mod.instHasKernels {S : SuperCommAlgebra} :

CategoryTheory.Limits.HasKernels S.Mod

Super modules have kernels, computed degreewise.

Cokernels #

theorem RS.SuperCommAlgebra.Mod.actEE_mem_range {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) (x : S.even) (n : N.even) (hn : n ∈ f.evenMap.range) :

(N.actEE x) n ∈ f.evenMap.range

theorem RS.SuperCommAlgebra.Mod.actEO_mem_range {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) (x : S.even) (n : N.odd) (hn : n ∈ f.oddMap.range) :

(N.actEO x) n ∈ f.oddMap.range

theorem RS.SuperCommAlgebra.Mod.actOE_mem_range {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) (v : S.odd) (n : N.even) (hn : n ∈ f.evenMap.range) :

(N.actOE v) n ∈ f.oddMap.range

theorem RS.SuperCommAlgebra.Mod.actOO_mem_range {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) (v : S.odd) (n : N.odd) (hn : n ∈ f.oddMap.range) :

(N.actOO v) n ∈ f.evenMap.range

def RS.SuperCommAlgebra.Mod.cokerMod {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) :

The cokernel of a morphism of super modules: the quotients of the two components by the two ranges, with the four action blocks descended.

Equations

One or more equations did not get rendered due to their size.

Instances For

def RS.SuperCommAlgebra.Mod.cokerProj {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) :

N ⟶ cokerMod f

The projection onto the cokernel of a morphism of super modules.

Equations

RS.SuperCommAlgebra.Mod.cokerProj f = { evenMap := f.evenMap.range.mkQ, oddMap := f.oddMap.range.mkQ, map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ }

Instances For

theorem RS.SuperCommAlgebra.Mod.comp_cokerProj {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) :

CategoryTheory.CategoryStruct.comp f (cokerProj f) = 0

theorem RS.SuperCommAlgebra.Mod.epi_cokerProj {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) :

CategoryTheory.Epi (cokerProj f)

The projection onto the cokernel is an epimorphism.

def RS.SuperCommAlgebra.Mod.cokerDesc {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) {W : S.Mod} (k : N ⟶ W) (hk : CategoryTheory.CategoryStruct.comp f k = 0) :

cokerMod f ⟶ W

The descent of a morphism annihilating f through the projection onto the cokernel.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem RS.SuperCommAlgebra.Mod.cokerProj_desc {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) {W : S.Mod} (k : N ⟶ W) (hk : CategoryTheory.CategoryStruct.comp f k = 0) :

CategoryTheory.CategoryStruct.comp (cokerProj f) (cokerDesc f k hk) = k

def RS.SuperCommAlgebra.Mod.cokernelCofork {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) :

CategoryTheory.Limits.CokernelCofork f

The cokernel cofork of a morphism of super modules.

Equations

RS.SuperCommAlgebra.Mod.cokernelCofork f = CategoryTheory.Limits.CokernelCofork.ofπ (RS.SuperCommAlgebra.Mod.cokerProj f) ⋯

Instances For

def RS.SuperCommAlgebra.Mod.cokernelCoforkIsColimit {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) :

CategoryTheory.Limits.IsColimit (cokernelCofork f)

The cokernel cofork is colimiting.

Equations

One or more equations did not get rendered due to their size.

Instances For

instance RS.SuperCommAlgebra.Mod.instHasCokernels {S : SuperCommAlgebra} :

CategoryTheory.Limits.HasCokernels S.Mod

Super modules have cokernels, computed degreewise.

The degreewise bridges #

theorem RS.SuperCommAlgebra.Mod.mono_iff {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) :

CategoryTheory.Mono f ↔ Function.Injective ⇑f.evenMap ∧ Function.Injective ⇑f.oddMap

A morphism of super modules is a monomorphism exactly when both of its components are injective.

theorem RS.SuperCommAlgebra.Mod.epi_iff {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) :

CategoryTheory.Epi f ↔ Function.Surjective ⇑f.evenMap ∧ Function.Surjective ⇑f.oddMap

A morphism of super modules is an epimorphism exactly when both of its components are surjective.

Normality #

noncomputable def RS.SuperCommAlgebra.Mod.monoLift {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) {W : S.Mod} (he : Function.Injective ⇑f.evenMap) (ho : Function.Injective ⇑f.oddMap) (k : W ⟶ N) (hme : ∀ (w : W.even), k.evenMap w ∈ f.evenMap.range) (hmo : ∀ (w : W.odd), k.oddMap w ∈ f.oddMap.range) :

W ⟶ M

The degreewise factorisation of a morphism annihilated by the projection onto the cokernel of a degreewise injective f.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem RS.SuperCommAlgebra.Mod.monoLift_comp {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) {W : S.Mod} (he : Function.Injective ⇑f.evenMap) (ho : Function.Injective ⇑f.oddMap) (k : W ⟶ N) (hme : ∀ (w : W.even), k.evenMap w ∈ f.evenMap.range) (hmo : ∀ (w : W.odd), k.oddMap w ∈ f.oddMap.range) :

CategoryTheory.CategoryStruct.comp (monoLift f he ho k hme hmo) f = k

theorem RS.SuperCommAlgebra.Mod.evenMap_mem_range {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) {W : S.Mod} (k : W ⟶ N) (hk : CategoryTheory.CategoryStruct.comp k (cokerProj f) = 0) (w : W.even) :

k.evenMap w ∈ f.evenMap.range

theorem RS.SuperCommAlgebra.Mod.oddMap_mem_range {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) {W : S.Mod} (k : W ⟶ N) (hk : CategoryTheory.CategoryStruct.comp k (cokerProj f) = 0) (w : W.odd) :

k.oddMap w ∈ f.oddMap.range

@[implicit_reducible]

noncomputable def RS.SuperCommAlgebra.Mod.normalMonoOfInjective {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) (he : Function.Injective ⇑f.evenMap) (ho : Function.Injective ⇑f.oddMap) :

CategoryTheory.NormalMono f

A degreewise injective morphism of super modules is the kernel of its cokernel.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def RS.SuperCommAlgebra.Mod.epiDesc {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) {W : S.Mod} (he : Function.Surjective ⇑f.evenMap) (ho : Function.Surjective ⇑f.oddMap) (k : M ⟶ W) (hke : ∀ (m : M.even), f.evenMap m = 0 → k.evenMap m = 0) (hko : ∀ (m : M.odd), f.oddMap m = 0 → k.oddMap m = 0) :

N ⟶ W

The degreewise factorisation of a morphism annihilating the inclusion of the kernel of a degreewise surjective f.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem RS.SuperCommAlgebra.Mod.comp_epiDesc {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) {W : S.Mod} (he : Function.Surjective ⇑f.evenMap) (ho : Function.Surjective ⇑f.oddMap) (k : M ⟶ W) (hke : ∀ (m : M.even), f.evenMap m = 0 → k.evenMap m = 0) (hko : ∀ (m : M.odd), f.oddMap m = 0 → k.oddMap m = 0) :

CategoryTheory.CategoryStruct.comp f (epiDesc f he ho k hke hko) = k

theorem RS.SuperCommAlgebra.Mod.evenMap_eq_zero_of_comp {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) {W : S.Mod} (k : M ⟶ W) (hk : CategoryTheory.CategoryStruct.comp (kerIncl f) k = 0) (m : M.even) (hm : f.evenMap m = 0) :

k.evenMap m = 0

theorem RS.SuperCommAlgebra.Mod.oddMap_eq_zero_of_comp {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) {W : S.Mod} (k : M ⟶ W) (hk : CategoryTheory.CategoryStruct.comp (kerIncl f) k = 0) (m : M.odd) (hm : f.oddMap m = 0) :

k.oddMap m = 0

@[implicit_reducible]

noncomputable def RS.SuperCommAlgebra.Mod.normalEpiOfSurjective {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) (he : Function.Surjective ⇑f.evenMap) (ho : Function.Surjective ⇑f.oddMap) :

CategoryTheory.NormalEpi f

A degreewise surjective morphism of super modules is the cokernel of its kernel.

Equations

One or more equations did not get rendered due to their size.

Instances For

Abelianness #

instance RS.SuperCommAlgebra.Mod.instIsNormalMonoCategory {S : SuperCommAlgebra} :

CategoryTheory.IsNormalMonoCategory S.Mod

Every monomorphism of super modules is a kernel.

instance RS.SuperCommAlgebra.Mod.instIsNormalEpiCategory {S : SuperCommAlgebra} :

CategoryTheory.IsNormalEpiCategory S.Mod

Every epimorphism of super modules is a cokernel.

instance RS.SuperCommAlgebra.Mod.instHasFiniteProducts {S : SuperCommAlgebra} :

CategoryTheory.Limits.HasFiniteProducts S.Mod

Super modules have finite products: they have a zero object and binary biproducts.

@[instance_reducible]

noncomputable instance RS.SuperCommAlgebra.Mod.instAbelian {S : SuperCommAlgebra} :

CategoryTheory.Abelian S.Mod

Modules over a super-commutative ℂ-algebra form an abelian category, with kernels, cokernels and biproducts all computed degreewise.

Equations

One or more equations did not get rendered due to their size.