Module

TwoChartCech_kerMap_injective_of_H0_eq_zero.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_kerMap_injective_of_H0_eq_zero

2 declarations indexed from sourceView source ↗

Module documentation

Injectivity of kernel base change when the base kernel vanishes.

Imports3

Nyll.SchemeTheory.Cohomology.Cech.TwoChartCech
Mathlib.RingTheory.Noetherian.Basic
Mathlib.RingTheory.Finiteness.Basic

Imported by2

theorem

exists_injective_linearMap

L44 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_kerMap_injective_of_H0_eq_zero.TwoChartCech.Snake.exists_injective_linearMap

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_kerMap_injective_of_H0_eq_zero
universe u
namespace TwoChartCech
namespace Snake
open _root_.TwoChartCech
variable {R : Type u} [CommRing R]
    {K0 K1 E0 E1 S0 S1 : Type u}
    [AddCommGroup K0] [Module R K0] [AddCommGroup K1] [Module R K1]
    [AddCommGroup E0] [Module R E0] [AddCommGroup E1] [Module R E1]
    [AddCommGroup S0] [Module R S0] [AddCommGroup S1] [Module R S1]
    (dK : K0 →ₗ[R] K1) (dE : E0 →ₗ[R] E1) (dS : S0 →ₗ[R] S1)
    (i0 : K0 →ₗ[R] E0) (i1 : K1 →ₗ[R] E1) (p0 : E0 →ₗ[R] S0) (p1 : E1 →ₗ[R] S1)
    (hi : dE ∘ₗ i0 = i1 ∘ₗ dK) (hp : dS ∘ₗ p0 = p1 ∘ₗ dE)
    (hi1 : Function.Injective i1) (hp0 : Function.Surjective p0)
    (hex0 : LinearMap.range i0 = LinearMap.ker p0) (hex1 : LinearMap.range i1 = LinearMap.ker p1)
    (hE : LinearMap.ker dE = ⊥)
include hi hp hi1 hp0 hex0 hex1 hE in

Lean source · statement

theorem exists_injective_linearMap :
    ∃ δ : LinearMap.ker dS →ₗ[R] (K1 ⧸ LinearMap.range dK), Function.Injective δ

theorem

kerMap_injective_of_H0_eq_zero

L108 ↗

TwoChartCech.kerMap_injective_of_H0_eq_zero

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_kerMap_injective_of_H0_eq_zero
universe u

Lean source · statement

theorem _root_.TwoChartCech.kerMap_injective_of_H0_eq_zero
    {R : Type u} [CommRing R] [IsNoetherianRing R]
    {K0 K1 E0 E1 S0 S1 : Type u}
    [AddCommGroup K0] [Module R K0] [AddCommGroup K1] [Module R K1]
    [AddCommGroup E0] [Module R E0] [AddCommGroup E1] [Module R E1]
    [AddCommGroup S0] [Module R S0] [AddCommGroup S1] [Module R S1]
    (dK : K0 →ₗ[R] K1) (dE : E0 →ₗ[R] E1) (dS : S0 →ₗ[R] S1)
    (i0 : K0 →ₗ[R] E0) (i1 : K1 →ₗ[R] E1) (p0 : E0 →ₗ[R] S0) (p1 : E1 →ₗ[R] S1)
    (hi : dE ∘ₗ i0 = i1 ∘ₗ dK) (hp : dS ∘ₗ p0 = p1 ∘ₗ dE)
    (hi1 : Function.Injective i1) (hp0 : Function.Surjective p0)
    (hex0 : LinearMap.range i0 = LinearMap.ker p0) (hex1 : LinearMap.range i1 = LinearMap.ker p1)
    (hE : LinearMap.ker dE = ⊥) [Module.Finite R (K1 ⧸ LinearMap.range dK)] :
    Module.Finite R (LinearMap.ker dS)

Module documentation

Declarations

exists_injective_linearMap

kerMap_injective_of_H0_eq_zero