Module.ker_baseChange_field_of_subsingleton_H1
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_ker_baseChange_field_of_subsingleton_H1
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] TwoChartCech.Sections.mk.injEq TwoChartCech.Cover.mk.injEq
TwoChartCech.GrothendieckComplex.mk.injEq TwoChartCech.Sections.mk.sizeOf_spec
TwoChartCech.Cover.mk.sizeOf_spec TwoChartCech.Cover.lineBundle_r0_apply
TwoChartCech.GrothendieckComplex.mk.sizeOf_spec TwoChartCech.Cover.lineBundle_r1_apply
CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec CoherentBaseChange.TwoTermComplex.mk.injEq
universe u
open TensorProductLean source · statement
theorem _root_.Module.ker_baseChange_field_of_subsingleton_H1
(R : Type u) [CommRing R] [IsNoetherianRing R]
(C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)] [∀ i, Module.Flat R (C i)]
(d : ∀ i, C i →ₗ[R] C (i + 1)) (hdd : ∀ i, d (i + 1) ∘ₗ d i = 0)
(n : ℕ) (hbdd : ∀ i, n < i → Subsingleton (C i))
(hfin0 : Module.Finite R (LinearMap.ker (d 0)))
(hfin : ∀ i, Module.Finite R
(LinearMap.ker (d (i + 1)) ⧸ (LinearMap.range (d i)).comap (LinearMap.ker (d (i +
1))).subtype))
(K : Type u) [Field K] [Algebra R K]
(hH1 : LinearMap.ker ((d 1).baseChange K) ≤ LinearMap.range ((d 0).baseChange K)) :
LinearMap.range ((LinearMap.ker (d 0)).subtype.baseChange K) = LinearMap.ker ((d 0).baseChange
K) ∧
Function.Injective ((LinearMap.ker (d 0)).subtype.baseChange K)