NYLL
Module

LinearMap_nonempty_kerModRange_equiv_of_equiv_comm.lean

Nyll.AlgebraicCurves.Foundations.Algebra.LinearMap_nonempty_kerModRange_equiv_of_equiv_comm
6 declarations indexed from sourceView source ↗

Module documentation

Linear Map nonempty ker Mod Range equiv of equiv comm

Imports2
  • Mathlib.LinearAlgebra.Quotient.Basic
  • Mathlib.Tactic.Ext
Imported by5

Declarations

theorem

kerModRange_map_ker

L40 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.LinearMap_nonempty_kerModRange_equiv_of_equiv_comm.LinearMap.kerModRange_map_ker
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearMap_nonempty_kerModRange_equiv_of_equiv_comm
universe u v w
namespace LinearMap
open _root_.LinearMap
open _root_.LinearMap
section KerModRange
variable {R : Type u} [CommRing R] {C : ℕ → Type v} {C' : ℕ → Type w}
  [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)] [∀ i, AddCommGroup (C' i)] [∀ i, Module R (C' i)]
  (d : ∀ i, C i →ₗ[R] C (i + 1)) (d' : ∀ i, C' i →ₗ[R] C' (i + 1))
  (e : ∀ i, C i ≃ₗ[R] C' i) (he : ∀ i x, e (i + 1) (d i x) = d' i (e i x))
include he
Lean source · statement
theorem kerModRange_map_ker (i : ℕ) :
    (LinearMap.ker (d i)).map (e i : C i →ₗ[R] C' i) = LinearMap.ker (d' i)
def

kerEquivOfComm

L53 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.LinearMap_nonempty_kerModRange_equiv_of_equiv_comm.LinearMap.kerEquivOfComm
Documentation

The kernel equivalence induced by a commuting family of componentwise linear equivalences.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearMap_nonempty_kerModRange_equiv_of_equiv_comm
universe u v w
namespace LinearMap
open _root_.LinearMap
open _root_.LinearMap
section KerModRange
variable {R : Type u} [CommRing R] {C : ℕ → Type v} {C' : ℕ → Type w}
  [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)] [∀ i, AddCommGroup (C' i)] [∀ i, Module R (C' i)]
  (d : ∀ i, C i →ₗ[R] C (i + 1)) (d' : ∀ i, C' i →ₗ[R] C' (i + 1))
  (e : ∀ i, C i ≃ₗ[R] C' i) (he : ∀ i x, e (i + 1) (d i x) = d' i (e i x))
include he
Lean source · statement
def kerEquivOfComm (i : ℕ) : LinearMap.ker (d i) ≃ₗ[R] LinearMap.ker (d' i)
theorem

kerEquivOfComm_apply

L57 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.LinearMap_nonempty_kerModRange_equiv_of_equiv_comm.LinearMap.kerEquivOfComm_apply
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearMap_nonempty_kerModRange_equiv_of_equiv_comm
universe u v w
namespace LinearMap
open _root_.LinearMap
open _root_.LinearMap
section KerModRange
variable {R : Type u} [CommRing R] {C : ℕ → Type v} {C' : ℕ → Type w}
  [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)] [∀ i, AddCommGroup (C' i)] [∀ i, Module R (C' i)]
  (d : ∀ i, C i →ₗ[R] C (i + 1)) (d' : ∀ i, C' i →ₗ[R] C' (i + 1))
  (e : ∀ i, C i ≃ₗ[R] C' i) (he : ∀ i x, e (i + 1) (d i x) = d' i (e i x))
include he
Lean source · statement
theorem kerEquivOfComm_apply (i : ℕ) (x : LinearMap.ker (d i)) :
    ((kerEquivOfComm d d' e he i x : LinearMap.ker (d' i)) : C' i) = e i x
theorem

kerModRange_map_comap

L60 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.LinearMap_nonempty_kerModRange_equiv_of_equiv_comm.LinearMap.kerModRange_map_comap
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearMap_nonempty_kerModRange_equiv_of_equiv_comm
universe u v w
namespace LinearMap
open _root_.LinearMap
open _root_.LinearMap
section KerModRange
variable {R : Type u} [CommRing R] {C : ℕ → Type v} {C' : ℕ → Type w}
  [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)] [∀ i, AddCommGroup (C' i)] [∀ i, Module R (C' i)]
  (d : ∀ i, C i →ₗ[R] C (i + 1)) (d' : ∀ i, C' i →ₗ[R] C' (i + 1))
  (e : ∀ i, C i ≃ₗ[R] C' i) (he : ∀ i x, e (i + 1) (d i x) = d' i (e i x))
include he
Lean source · statement
theorem kerModRange_map_comap (i : ℕ) :
    ((LinearMap.range (d i)).comap (LinearMap.ker (d (i + 1))).subtype).map
        (kerEquivOfComm d d' e he (i + 1) : LinearMap.ker (d (i + 1)) →ₗ[R] LinearMap.ker (d' (i +
          1)))
      = (LinearMap.range (d' i)).comap (LinearMap.ker (d' (i + 1))).subtype
theorem

nonempty_kerModRange_equiv_of_equiv_comm'

L83 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.LinearMap_nonempty_kerModRange_equiv_of_equiv_comm.LinearMap.nonempty_kerModRange_equiv_of_equiv_comm'
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearMap_nonempty_kerModRange_equiv_of_equiv_comm
universe u v w
namespace LinearMap
open _root_.LinearMap
open _root_.LinearMap
section KerModRange
variable {R : Type u} [CommRing R] {C : ℕ → Type v} {C' : ℕ → Type w}
  [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)] [∀ i, AddCommGroup (C' i)] [∀ i, Module R (C' i)]
  (d : ∀ i, C i →ₗ[R] C (i + 1)) (d' : ∀ i, C' i →ₗ[R] C' (i + 1))
  (e : ∀ i, C i ≃ₗ[R] C' i) (he : ∀ i x, e (i + 1) (d i x) = d' i (e i x))
include he
Lean source · statement
theorem nonempty_kerModRange_equiv_of_equiv_comm' :
    Nonempty (LinearMap.ker (d 0) ≃ₗ[R] LinearMap.ker (d' 0)) ∧
    ∀ i, Nonempty
      ((LinearMap.ker (d (i + 1)) ⧸ (LinearMap.range (d i)).comap (LinearMap.ker (d (i +
        1))).subtype) ≃ₗ[R]
       (LinearMap.ker (d' (i + 1)) ⧸ (LinearMap.range (d' i)).comap (LinearMap.ker (d' (i +
         1))).subtype))
theorem

nonempty_kerModRange_equiv_of_equiv_comm

L98 ↗
LinearMap.nonempty_kerModRange_equiv_of_equiv_comm
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearMap_nonempty_kerModRange_equiv_of_equiv_comm
universe u v w
Lean source · statement
theorem _root_.LinearMap.nonempty_kerModRange_equiv_of_equiv_comm
    {R : Type u} [CommRing R] {C C' : ℕ → Type u}
    [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)] [∀ i, AddCommGroup (C' i)] [∀ i, Module R (C'
      i)]
    (d : ∀ i, C i →ₗ[R] C (i + 1)) (d' : ∀ i, C' i →ₗ[R] C' (i + 1))
    (e : ∀ i, C i ≃ₗ[R] C' i) (he : ∀ i x, e (i + 1) (d i x) = d' i (e i x)) :
    Nonempty (LinearMap.ker (d 0) ≃ₗ[R] LinearMap.ker (d' 0)) ∧
    ∀ i, Nonempty
      ((LinearMap.ker (d (i + 1)) ⧸ (LinearMap.range (d i)).comap (LinearMap.ker (d (i +
        1))).subtype) ≃ₗ[R]
       (LinearMap.ker (d' (i + 1)) ⧸ (LinearMap.range (d' i)).comap (LinearMap.ker (d' (i +
         1))).subtype))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.