Module

LinearMap_sum_neg_one_pow_mul_finrank_eq_zero_of_exact.lean

Nyll.AlgebraicCurves.Foundations.Algebra.LinearMap_sum_neg_one_pow_mul_finrank_eq_zero_of_exact

3 declarations indexed from sourceView source ↗

Module documentation

Linear Map sum neg one pow mul finrank eq zero of exact

Imports3

Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.SimpRw

Imported by2

theorem

finrank_eq_range_add_ker

L34 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearMap_sum_neg_one_pow_mul_finrank_eq_zero_of_exact.P2mLES.finrank_eq_range_add_ker

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearMap_sum_neg_one_pow_mul_finrank_eq_zero_of_exact
open Module
universe u v
namespace P2mLES
variable {k : Type u} [DivisionRing k]

Lean source · statement

theorem finrank_eq_range_add_ker {M N : Type v} [AddCommGroup M] [Module k M] [AddCommGroup N]
  [Module k N]
    [Module.Finite k M] (f : M →ₗ[k] N) :
    finrank k M = finrank k (LinearMap.range f) + finrank k (LinearMap.ker f)

theorem

main

L40 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearMap_sum_neg_one_pow_mul_finrank_eq_zero_of_exact.P2mLES.main

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearMap_sum_neg_one_pow_mul_finrank_eq_zero_of_exact
open Module
universe u v
namespace P2mLES
variable {k : Type u} [DivisionRing k]

Lean source · statement

theorem main
    (A B C : ℕ → Type v)
    [∀ i, AddCommGroup (A i)] [∀ i, Module k (A i)] [∀ i, Module.Finite k (A i)]
    [∀ i, AddCommGroup (B i)] [∀ i, Module k (B i)] [∀ i, Module.Finite k (B i)]
    [∀ i, AddCommGroup (C i)] [∀ i, Module k (C i)] [∀ i, Module.Finite k (C i)]
    (f : ∀ i, A i →ₗ[k] B i) (g : ∀ i, B i →ₗ[k] C i) (δ : ∀ i, C i →ₗ[k] A (i + 1))
    (hf0 : Function.Injective (f 0))
    (hfg : ∀ i, Function.Exact (f i) (g i))
    (hgδ : ∀ i, Function.Exact (g i) (δ i))
    (hδf : ∀ i, Function.Exact (δ i) (f (i + 1)))
    (N : ℕ) (hN : Subsingleton (A N)) :
    ∑ i ∈ Finset.range N, (-1 : ℤ) ^ i *
        ((finrank k (A i) : ℤ) - finrank k (B i) + finrank k (C i)) = 0

theorem

sum_neg_one_pow_mul_finrank_eq_zero_of_exact

L97 ↗

LinearMap.sum_neg_one_pow_mul_finrank_eq_zero_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_sum_neg_one_pow_mul_finrank_eq_zero_of_exact
open Module
universe u v

Lean source · statement

theorem _root_.LinearMap.sum_neg_one_pow_mul_finrank_eq_zero_of_exact
    {k : Type u} [DivisionRing k] (A B C : ℕ → Type v)
    [∀ i, AddCommGroup (A i)] [∀ i, Module k (A i)] [∀ i, Module.Finite k (A i)]
    [∀ i, AddCommGroup (B i)] [∀ i, Module k (B i)] [∀ i, Module.Finite k (B i)]
    [∀ i, AddCommGroup (C i)] [∀ i, Module k (C i)] [∀ i, Module.Finite k (C i)]
    (f : ∀ i, A i →ₗ[k] B i) (g : ∀ i, B i →ₗ[k] C i) (δ : ∀ i, C i →ₗ[k] A (i + 1))
    (hf0 : Function.Injective (f 0))
    (hfg : ∀ i, Function.Exact (f i) (g i))
    (hgδ : ∀ i, Function.Exact (g i) (δ i))
    (hδf : ∀ i, Function.Exact (δ i) (f (i + 1)))
    (N : ℕ) (hN : Subsingleton (A N)) :
    ∑ i ∈ Finset.range N, (-1 : ℤ) ^ i *
        ((Module.finrank k (A i) : ℤ) - Module.finrank k (B i) + Module.finrank k (C i)) = 0

Module documentation

Linear Map sum neg one pow mul finrank eq zero of exact

Declarations

finrank_eq_range_add_ker

main

sum_neg_one_pow_mul_finrank_eq_zero_of_exact