Presentation of a cokernel #
If f : M₁ →ₗ[A] M₂ is a linear map between modules,
pres₂ is a presentation of M₂ and g₁ : ι → M₁ is
a family of generators of M₁ (which is expressed as
hg₁ : Submodule.span A (Set.range g₁) = ⊤), then we
provide a way to obtain a presentation of the cokernel of f.
It requires an additional data data : pres₂.CokernelData f g₁,
which consists of liftings of the images by f of
the generators of M₁ as linear combinations of the
generators of M₂. Then, we obtain a presentation
pres₂.cokernel data hg₁ : Presentation A (M₂ ⧸ LinearMap.range f).
More generally, if we have an exact sequence M₁ → M₂ → M₃ → 0,
we obtain a presentation of M₃, see Presentation.ofExact.
structure
Module.Presentation.CokernelData
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
(pres₂ : Module.Presentation A M₂)
(f : M₁ →ₗ[A] M₂)
{ι : Type w₁}
(g₁ : ι → M₁)
:
Type (max (max u w₁) w₂₀)
Given a linear map f : M₁ →ₗ[A] M₂, a presentation of M₂ and a choice
of generators of M₁, this structure specifies a lifting of the image by f
of each generator of M₁ as a linear combination of the generators of M₂.
- lift (i : ι) : pres₂.G →₀ A
a lifting of
f (g₁ i)inpres₂.G →₀ A - π_lift (i : ι) : pres₂.π (self.lift i) = f (g₁ i)
Instances For
def
Module.Presentation.CokernelData.ofSection
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
(pres₂ : Module.Presentation A M₂)
(f : M₁ →ₗ[A] M₂)
{ι : Type w₁}
(g₁ : ι → M₁)
(s : M₂ → pres₂.G →₀ A)
(hs : ∀ (m₂ : M₂), pres₂.π (s m₂) = m₂)
:
pres₂.CokernelData f g₁
Constructor for Presentation.CokernelData in case we have a chosen set-theoretic
section of the projection (pres₂.G →₀ A) → M₂.
Equations
- Module.Presentation.CokernelData.ofSection pres₂ f g₁ s hs = { lift := fun (i : ι) => s (f (g₁ i)), π_lift := ⋯ }
Instances For
@[simp]
theorem
Module.Presentation.CokernelData.ofSection_lift
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
(pres₂ : Module.Presentation A M₂)
(f : M₁ →ₗ[A] M₂)
{ι : Type w₁}
(g₁ : ι → M₁)
(s : M₂ → pres₂.G →₀ A)
(hs : ∀ (m₂ : M₂), pres₂.π (s m₂) = m₂)
(i : ι)
:
(Module.Presentation.CokernelData.ofSection pres₂ f g₁ s hs).lift i = s (f (g₁ i))
instance
Module.Presentation.nonempty_cokernelData
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
(pres₂ : Module.Presentation A M₂)
(f : M₁ →ₗ[A] M₂)
{ι : Type w₁}
(g₁ : ι → M₁)
:
Nonempty (pres₂.CokernelData f g₁)
def
Module.Presentation.cokernelRelations
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
(pres₂ : Module.Presentation A M₂)
{f : M₁ →ₗ[A] M₂}
{ι : Type w₁}
{g₁ : ι → M₁}
(data : pres₂.CokernelData f g₁)
:
The shape of the presentation by generators and relations of the cokernel
of f : M₁ →ₗ[A] M₂. It consists of a generator for each generator of M₂, and
there are two types of relations: one for each relation in the presentation in M₂,
and one for each generator of M₁.
Equations
Instances For
@[simp]
theorem
Module.Presentation.cokernelRelations_R
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
(pres₂ : Module.Presentation A M₂)
{f : M₁ →ₗ[A] M₂}
{ι : Type w₁}
{g₁ : ι → M₁}
(data : pres₂.CokernelData f g₁)
:
@[simp]
theorem
Module.Presentation.cokernelRelations_relation
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
(pres₂ : Module.Presentation A M₂)
{f : M₁ →ₗ[A] M₂}
{ι : Type w₁}
{g₁ : ι → M₁}
(data : pres₂.CokernelData f g₁)
(x : pres₂.R ⊕ ι)
:
@[simp]
theorem
Module.Presentation.cokernelRelations_G
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
(pres₂ : Module.Presentation A M₂)
{f : M₁ →ₗ[A] M₂}
{ι : Type w₁}
{g₁ : ι → M₁}
(data : pres₂.CokernelData f g₁)
:
(pres₂.cokernelRelations data).G = pres₂.G
def
Module.Presentation.cokernelSolution
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
(pres₂ : Module.Presentation A M₂)
{f : M₁ →ₗ[A] M₂}
{ι : Type w₁}
{g₁ : ι → M₁}
(data : pres₂.CokernelData f g₁)
:
(pres₂.cokernelRelations data).Solution (M₂ ⧸ LinearMap.range f)
The obvious solution in M₂ ⧸ LinearMap.range f to the equations in
pres₂.cokernelRelations data.
Equations
- pres₂.cokernelSolution data = { var := fun (g : (pres₂.cokernelRelations data).G) => (LinearMap.range f).mkQ (pres₂.var g), linearCombination_var_relation := ⋯ }
Instances For
@[simp]
theorem
Module.Presentation.cokernelSolution_var
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
(pres₂ : Module.Presentation A M₂)
{f : M₁ →ₗ[A] M₂}
{ι : Type w₁}
{g₁ : ι → M₁}
(data : pres₂.CokernelData f g₁)
(g : (pres₂.cokernelRelations data).G)
:
(pres₂.cokernelSolution data).var g = (LinearMap.range f).mkQ (pres₂.var g)
noncomputable def
Module.Presentation.cokernelSolution.isPresentationCore
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
(pres₂ : Module.Presentation A M₂)
{f : M₁ →ₗ[A] M₂}
{ι : Type w₁}
{g₁ : ι → M₁}
(data : pres₂.CokernelData f g₁)
(hg₁ : Submodule.span A (Set.range g₁) = ⊤)
:
(pres₂.cokernelSolution data).IsPresentationCore
The cokernel can be defined by generators and relations.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Module.Presentation.cokernelSolution.isPresentation
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
(pres₂ : Module.Presentation A M₂)
{f : M₁ →ₗ[A] M₂}
{ι : Type w₁}
{g₁ : ι → M₁}
(data : pres₂.CokernelData f g₁)
(hg₁ : Submodule.span A (Set.range g₁) = ⊤)
:
(pres₂.cokernelSolution data).IsPresentation
def
Module.Presentation.cokernel
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
(pres₂ : Module.Presentation A M₂)
{f : M₁ →ₗ[A] M₂}
{ι : Type w₁}
{g₁ : ι → M₁}
(data : pres₂.CokernelData f g₁)
(hg₁ : Submodule.span A (Set.range g₁) = ⊤)
:
Module.Presentation A (M₂ ⧸ LinearMap.range f)
The presentation of the cokernel of a linear map f : M₁ →ₗ[A] M₂ that is obtained
from a presentation pres₂ of M₂, a choice of generators g₁ : ι → M₁ of M₁,
and an additional data in pres₂.CokernelData f g₁.
Equations
- pres₂.cokernel data hg₁ = Module.Presentation.ofIsPresentation ⋯
Instances For
@[simp]
theorem
Module.Presentation.cokernel_G
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
(pres₂ : Module.Presentation A M₂)
{f : M₁ →ₗ[A] M₂}
{ι : Type w₁}
{g₁ : ι → M₁}
(data : pres₂.CokernelData f g₁)
(hg₁ : Submodule.span A (Set.range g₁) = ⊤)
:
(pres₂.cokernel data hg₁).G = pres₂.G
@[simp]
theorem
Module.Presentation.cokernel_var
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
(pres₂ : Module.Presentation A M₂)
{f : M₁ →ₗ[A] M₂}
{ι : Type w₁}
{g₁ : ι → M₁}
(data : pres₂.CokernelData f g₁)
(hg₁ : Submodule.span A (Set.range g₁) = ⊤)
(g : (pres₂.cokernelRelations data).G)
:
(pres₂.cokernel data hg₁).var g = Submodule.Quotient.mk (pres₂.var g)
@[simp]
theorem
Module.Presentation.cokernel_R
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
(pres₂ : Module.Presentation A M₂)
{f : M₁ →ₗ[A] M₂}
{ι : Type w₁}
{g₁ : ι → M₁}
(data : pres₂.CokernelData f g₁)
(hg₁ : Submodule.span A (Set.range g₁) = ⊤)
:
@[simp]
theorem
Module.Presentation.cokernel_relation
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
(pres₂ : Module.Presentation A M₂)
{f : M₁ →ₗ[A] M₂}
{ι : Type w₁}
{g₁ : ι → M₁}
(data : pres₂.CokernelData f g₁)
(hg₁ : Submodule.span A (Set.range g₁) = ⊤)
(r : (pres₂.cokernelRelations data).R)
:
noncomputable def
Module.Presentation.ofExact
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
{M₃ : Type v₃}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
[AddCommGroup M₃]
[Module A M₃]
{f : M₁ →ₗ[A] M₂}
{g : M₂ →ₗ[A] M₃}
(pres₂ : Module.Presentation A M₂)
{ι : Type w₁}
{g₁ : ι → M₁}
(data : pres₂.CokernelData f g₁)
(hfg : Function.Exact ⇑f ⇑g)
(hg : Function.Surjective ⇑g)
(hg₁ : Submodule.span A (Set.range g₁) = ⊤)
:
Module.Presentation A M₃
Given an exact sequence of A-modules M₁ → M₂ → M₃ → 0, this is the presentation
of M₃ that is obtained from a presentation pres₂ of M₂, a choice of generators
g₁ : ι → M₁ of M₁, and an additional data in a Presentation.CokernelData structure.
Equations
- pres₂.ofExact data hfg hg hg₁ = (pres₂.cokernel data hg₁).ofLinearEquiv (hfg.linearEquivOfSurjective hg)
Instances For
@[simp]
theorem
Module.Presentation.ofExact_R
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
{M₃ : Type v₃}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
[AddCommGroup M₃]
[Module A M₃]
{f : M₁ →ₗ[A] M₂}
{g : M₂ →ₗ[A] M₃}
(pres₂ : Module.Presentation A M₂)
{ι : Type w₁}
{g₁ : ι → M₁}
(data : pres₂.CokernelData f g₁)
(hfg : Function.Exact ⇑f ⇑g)
(hg : Function.Surjective ⇑g)
(hg₁ : Submodule.span A (Set.range g₁) = ⊤)
:
@[simp]
theorem
Module.Presentation.ofExact_G
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
{M₃ : Type v₃}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
[AddCommGroup M₃]
[Module A M₃]
{f : M₁ →ₗ[A] M₂}
{g : M₂ →ₗ[A] M₃}
(pres₂ : Module.Presentation A M₂)
{ι : Type w₁}
{g₁ : ι → M₁}
(data : pres₂.CokernelData f g₁)
(hfg : Function.Exact ⇑f ⇑g)
(hg : Function.Surjective ⇑g)
(hg₁ : Submodule.span A (Set.range g₁) = ⊤)
:
(pres₂.ofExact data hfg hg hg₁).G = pres₂.G
@[simp]
theorem
Module.Presentation.ofExact_var
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
{M₃ : Type v₃}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
[AddCommGroup M₃]
[Module A M₃]
{f : M₁ →ₗ[A] M₂}
{g : M₂ →ₗ[A] M₃}
(pres₂ : Module.Presentation A M₂)
{ι : Type w₁}
{g₁ : ι → M₁}
(data : pres₂.CokernelData f g₁)
(hfg : Function.Exact ⇑f ⇑g)
(hg : Function.Surjective ⇑g)
(hg₁ : Submodule.span A (Set.range g₁) = ⊤)
(g✝ : (pres₂.cokernel data hg₁).G)
:
(pres₂.ofExact data hfg hg hg₁).var g✝ = g (pres₂.var g✝)
@[simp]
theorem
Module.Presentation.ofExact_relation
{A : Type u}
[Ring A]
{M₁ : Type v₁}
{M₂ : Type v₂}
{M₃ : Type v₃}
[AddCommGroup M₁]
[Module A M₁]
[AddCommGroup M₂]
[Module A M₂]
[AddCommGroup M₃]
[Module A M₃]
{f : M₁ →ₗ[A] M₂}
{g : M₂ →ₗ[A] M₃}
(pres₂ : Module.Presentation A M₂)
{ι : Type w₁}
{g₁ : ι → M₁}
(data : pres₂.CokernelData f g₁)
(hfg : Function.Exact ⇑f ⇑g)
(hg : Function.Surjective ⇑g)
(hg₁ : Submodule.span A (Set.range g₁) = ⊤)
(r : (pres₂.cokernel data hg₁).R)
: