Module

LinearMap_finrank_ker_sub_finrank_quotient_range_eq_add_of_exact.lean

Nyll.AlgebraicCurves.Foundations.Algebra.LinearMap_finrank_ker_sub_finrank_quotient_range_eq_add_of_exact

3 declarations indexed from sourceView source ↗

Module documentation

Relate kernel and cokernel dimensions along an exact sequence.

Imports2

Mathlib.Algebra.Module.SnakeLemma
Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Imported by2

lemma

finiteDimensional_of_exact

L35 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearMap_finrank_ker_sub_finrank_quotient_range_eq_add_of_exact.C2EulerCharAux.finiteDimensional_of_exact

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearMap_finrank_ker_sub_finrank_quotient_range_eq_add_of_exact
namespace C2EulerCharAux
open Function
universe u₀ u₁ u₂ u₃
variable {k : Type u₀} [DivisionRing k]
  {M : Type u₁} {N : Type u₂} {P : Type u₃}
  [AddCommGroup M] [Module k M] [AddCommGroup N] [Module k N] [AddCommGroup P] [Module k P]

Lean source · statement

lemma finiteDimensional_of_exact {f : M →ₗ[k] N} {g : N →ₗ[k] P} (h : Exact f g)
    [FiniteDimensional k M] [FiniteDimensional k P] : FiniteDimensional k N

lemma

finrank_eq_of_exact

L41 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearMap_finrank_ker_sub_finrank_quotient_range_eq_add_of_exact.C2EulerCharAux.finrank_eq_of_exact

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearMap_finrank_ker_sub_finrank_quotient_range_eq_add_of_exact
namespace C2EulerCharAux
open Function
universe u₀ u₁ u₂ u₃
variable {k : Type u₀} [DivisionRing k]
  {M : Type u₁} {N : Type u₂} {P : Type u₃}
  [AddCommGroup M] [Module k M] [AddCommGroup N] [Module k N] [AddCommGroup P] [Module k P]

Lean source · statement

lemma finrank_eq_of_exact {f : M →ₗ[k] N} {g : N →ₗ[k] P} (h : Exact f g)
    [FiniteDimensional k N] :
    Module.finrank k N
      = Module.finrank k (LinearMap.range f) + Module.finrank k (LinearMap.range g)

theorem

finrank_ker_sub_finrank_quotient_range_eq_add_of_exact

L52 ↗

LinearMap.finrank_ker_sub_finrank_quotient_range_eq_add_of_exact

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearMap_finrank_ker_sub_finrank_quotient_range_eq_add_of_exact
universe u v
open C2EulerCharAux in

Lean source · statement

theorem _root_.LinearMap.finrank_ker_sub_finrank_quotient_range_eq_add_of_exact
    {k : Type u} [Field k]
    {A₁ A₂ A₃ B₁ B₂ B₃ : Type v}
    [AddCommGroup A₁] [Module k A₁] [AddCommGroup A₂] [Module k A₂] [AddCommGroup A₃] [Module k A₃]
    [AddCommGroup B₁] [Module k B₁] [AddCommGroup B₂] [Module k B₂] [AddCommGroup B₃] [Module k B₃]
    (d₁ : A₁ →ₗ[k] B₁) (d₂ : A₂ →ₗ[k] B₂) (d₃ : A₃ →ₗ[k] B₃)
    (f₁ : A₁ →ₗ[k] A₂) (f₂ : A₂ →ₗ[k] A₃) (g₁ : B₁ →ₗ[k] B₂) (g₂ : B₂ →ₗ[k] B₃)
    (hf₁ : Function.Injective f₁) (hf : Function.Exact f₁ f₂) (hf₂ : Function.Surjective f₂)
    (hg₁ : Function.Injective g₁) (hg : Function.Exact g₁ g₂) (hg₂ : Function.Surjective g₂)
    (h₁ : g₁ ∘ₗ d₁ = d₂ ∘ₗ f₁) (h₂ : g₂ ∘ₗ d₂ = d₃ ∘ₗ f₂)
    [FiniteDimensional k (LinearMap.ker d₁)] [FiniteDimensional k (B₁ ⧸ LinearMap.range d₁)]
    [FiniteDimensional k (LinearMap.ker d₃)] [FiniteDimensional k (B₃ ⧸ LinearMap.range d₃)] :
    FiniteDimensional k (LinearMap.ker d₂) ∧ FiniteDimensional k (B₂ ⧸ LinearMap.range d₂) ∧
    (Module.finrank k (LinearMap.ker d₂) : ℤ) - Module.finrank k (B₂ ⧸ LinearMap.range d₂)
      = ((Module.finrank k (LinearMap.ker d₁) : ℤ) - Module.finrank k (B₁ ⧸ LinearMap.range d₁))
        + ((Module.finrank k (LinearMap.ker d₃) : ℤ) - Module.finrank k (B₃ ⧸ LinearMap.range
          d₃))

Module documentation

Declarations

finiteDimensional_of_exact

finrank_eq_of_exact

finrank_ker_sub_finrank_quotient_range_eq_add_of_exact