NYLL
Module

Module_ker_baseChange_field_of_subsingleton_H1_of_projective.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Module_ker_baseChange_field_of_subsingleton_H1_of_projective
7 declarations indexed from sourceView source ↗

Module documentation

Module ker base Change field of subsingleton H1 of projective

Imports3
Imported by2

Declarations

theorem

exact_of_equiv

L39 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_ker_baseChange_field_of_subsingleton_H1_of_projective.BC0Pt.exact_of_equiv
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_ker_baseChange_field_of_subsingleton_H1_of_projective
universe u v
open TensorProduct
namespace BC0Pt
section Transfer
variable {S : Type*} [CommRing S]
  {A B C A' B' C' : Type*} [AddCommGroup A] [Module S A] [AddCommGroup B] [Module S B]
    [AddCommGroup C] [Module S C]
  [AddCommGroup A'] [Module S A'] [AddCommGroup B'] [Module S B'] [AddCommGroup C'] [Module S C']
Lean source · statement
theorem exact_of_equiv (f : A →ₗ[S] B) (g : B →ₗ[S] C) (f' : A' →ₗ[S] B') (g' : B' →ₗ[S] C')
    (eA : A ≃ₗ[S] A') (eB : B ≃ₗ[S] B') (eC : C ≃ₗ[S] C')
    (hf : ∀ a, eB (f a) = f' (eA a)) (hg : ∀ b, eC (g b) = g' (eB b)) (h : Function.Exact f g) :
    Function.Exact f' g'
theorem

injective_of_equiv

L58 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_ker_baseChange_field_of_subsingleton_H1_of_projective.BC0Pt.injective_of_equiv
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_ker_baseChange_field_of_subsingleton_H1_of_projective
universe u v
open TensorProduct
namespace BC0Pt
section Transfer
variable {S : Type*} [CommRing S]
  {A B C A' B' C' : Type*} [AddCommGroup A] [Module S A] [AddCommGroup B] [Module S B]
    [AddCommGroup C] [Module S C]
  [AddCommGroup A'] [Module S A'] [AddCommGroup B'] [Module S B'] [AddCommGroup C'] [Module S C']
Lean source · statement
theorem injective_of_equiv (f : A →ₗ[S] B) (f' : A' →ₗ[S] B') (eA : A ≃ₗ[S] A') (eB : B ≃ₗ[S] B')
    (hf : ∀ a, eB (f a) = f' (eA a)) (h : Function.Injective f) : Function.Injective f'
theorem

ker_eq_range_and_injective_of_equiv

L66 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_ker_baseChange_field_of_subsingleton_H1_of_projective.BC0Pt.ker_eq_range_and_injective_of_equiv
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_ker_baseChange_field_of_subsingleton_H1_of_projective
universe u v
open TensorProduct
namespace BC0Pt
section Transfer
variable {S : Type*} [CommRing S]
  {A B C A' B' C' : Type*} [AddCommGroup A] [Module S A] [AddCommGroup B] [Module S B]
    [AddCommGroup C] [Module S C]
  [AddCommGroup A'] [Module S A'] [AddCommGroup B'] [Module S B'] [AddCommGroup C'] [Module S C']
Lean source · statement
theorem ker_eq_range_and_injective_of_equiv (f : A →ₗ[S] B) (g : B →ₗ[S] C) (f' : A' →ₗ[S] B') (g'
  : B' →ₗ[S] C')
    (eA : A ≃ₗ[S] A') (eB : B ≃ₗ[S] B') (eC : C ≃ₗ[S] C')
    (hf : ∀ a, eB (f a) = f' (eA a)) (hg : ∀ b, eC (g b) = g' (eB b))
    (h : LinearMap.range f = LinearMap.ker g ∧ Function.Injective f) :
    LinearMap.range f' = LinearMap.ker g' ∧ Function.Injective f'
abbrev

can

L86 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_ker_baseChange_field_of_subsingleton_H1_of_projective.BC0Pt.can
Documentation

The linear equivalence cancelling the intermediate scalar-extension step.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_ker_baseChange_field_of_subsingleton_H1_of_projective
universe u v
open TensorProduct
namespace BC0Pt
section Cancel
variable (R : Type*) [CommRing R] (A : Type*) [CommRing A] [Algebra R A] (B : Type*) [CommRing B]
  [Algebra R B]
  [Algebra A B] [IsScalarTower R A B]
  {M N : Type*} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N)
Lean source · statement
abbrev can (M : Type*) [AddCommGroup M] [Module R M] : B ⊗[A] (A ⊗[R] M) ≃ₗ[B] B ⊗[R]
  M
theorem

can_nat

L90 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_ker_baseChange_field_of_subsingleton_H1_of_projective.BC0Pt.can_nat
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_ker_baseChange_field_of_subsingleton_H1_of_projective
universe u v
open TensorProduct
namespace BC0Pt
section Cancel
variable (R : Type*) [CommRing R] (A : Type*) [CommRing A] [Algebra R A] (B : Type*) [CommRing B]
  [Algebra R B]
  [Algebra A B] [IsScalarTower R A B]
  {M N : Type*} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N)
Lean source · statement
theorem can_nat (z : B ⊗[A] (A ⊗[R] M)) :
    can R A B N ((f.baseChange A).baseChange B z) = f.baseChange B (can R A B M z)
theorem

main

L104 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_ker_baseChange_field_of_subsingleton_H1_of_projective.BC0Pt.main
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_ker_baseChange_field_of_subsingleton_H1_of_projective
universe u v
open TensorProduct
namespace BC0Pt
Lean source · statement
theorem main
    (R : Type u) [CommRing R]
    {C0 C1 C2 : Type v} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
    [AddCommGroup C2] [Module R C2]
    [Module.Finite R C1] [Module.Projective R C1] [Module.Finite R C2] [Module.Projective R C2]
    (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hdd : d1 ∘ₗ d0 = 0)
    (K : Type u) [Field K] [Algebra R K]
    (hH1 : LinearMap.ker (d1.baseChange K) ≤ LinearMap.range (d0.baseChange K)) :
    LinearMap.range ((LinearMap.ker d0).subtype.baseChange K) = LinearMap.ker (d0.baseChange K) ∧
      Function.Injective ((LinearMap.ker d0).subtype.baseChange K)
theorem

ker_baseChange_field_of_subsingleton_H1_of_projective

L230 ↗
Module.ker_baseChange_field_of_subsingleton_H1_of_projective
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_ker_baseChange_field_of_subsingleton_H1_of_projective
universe u v
open TensorProduct
Lean source · statement
theorem _root_.Module.ker_baseChange_field_of_subsingleton_H1_of_projective
    (R : Type u) [CommRing R]
    {C0 C1 C2 : Type v} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
    [AddCommGroup C2] [Module R C2]
    [Module.Finite R C1] [Module.Projective R C1] [Module.Finite R C2] [Module.Projective R C2]
    (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hdd : d1 ∘ₗ d0 = 0)
    (K : Type u) [Field K] [Algebra R K]
    (hH1 : LinearMap.ker (d1.baseChange K) ≤ LinearMap.range (d0.baseChange K)) :
    LinearMap.range ((LinearMap.ker d0).subtype.baseChange K) = LinearMap.ker (d0.baseChange K) ∧
      Function.Injective ((LinearMap.ker d0).subtype.baseChange K)

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