Module

Module_free_quotient_range_of_ker_baseChange_residueField_le.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Module_free_quotient_range_of_ker_baseChange_residueField_le

5 declarations indexed from sourceView source ↗

Module documentation

Module free quotient range of ker base Change residue Field le

Imports1

Mathlib.RingTheory.LocalRing.Module

Imported by3

theorem

rangeRestrict_comp_ker_subtype

L33 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_free_quotient_range_of_ker_baseChange_residueField_le.P2mKcTorCrit.rangeRestrict_comp_ker_subtype

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_free_quotient_range_of_ker_baseChange_residueField_le
open scoped TensorProduct
universe u v w
namespace P2mKcTorCrit
variable {R : Type u} [CommRing R]
variable {M : Type v} {N : Type w} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]

Lean source · statement

theorem rangeRestrict_comp_ker_subtype (f : M →ₗ[R] N) :
    f.rangeRestrict.comp (LinearMap.ker f).subtype = 0

theorem

subtype_comp_rangeRestrict

L39 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_free_quotient_range_of_ker_baseChange_residueField_le.P2mKcTorCrit.subtype_comp_rangeRestrict

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_free_quotient_range_of_ker_baseChange_residueField_le
open scoped TensorProduct
universe u v w
namespace P2mKcTorCrit
variable {R : Type u} [CommRing R]
variable {M : Type v} {N : Type w} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]

Lean source · statement

theorem subtype_comp_rangeRestrict (f : M →ₗ[R] N) :
    (LinearMap.range f).subtype.comp f.rangeRestrict = f

theorem

lTensor_subtype_range_injective

L43 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_free_quotient_range_of_ker_baseChange_residueField_le.P2mKcTorCrit.lTensor_subtype_range_injective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_free_quotient_range_of_ker_baseChange_residueField_le
open scoped TensorProduct
universe u v w
namespace P2mKcTorCrit
variable {R : Type u} [CommRing R]
variable {M : Type v} {N : Type w} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]

Lean source · statement

theorem lTensor_subtype_range_injective (A : Type*) [CommRing A] [Algebra R A] (f : M →ₗ[R] N)
    (h : LinearMap.ker (f.baseChange A) ≤
      LinearMap.range ((LinearMap.ker f).subtype.baseChange A)) :
    Function.Injective ((LinearMap.range f).subtype.lTensor A)

theorem

free_quotient_range

L62 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_free_quotient_range_of_ker_baseChange_residueField_le.P2mKcTorCrit.free_quotient_range

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_free_quotient_range_of_ker_baseChange_residueField_le
open scoped TensorProduct
universe u v w
namespace P2mKcTorCrit
variable {R : Type u} [CommRing R]
variable {M : Type v} {N : Type w} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]

Lean source · statement

theorem free_quotient_range [IsLocalRing R] [Module.Finite R M] [Module.Finite R N]
    [Module.Free R N] (f : M →ₗ[R] N)
    (h : LinearMap.ker (f.baseChange (IsLocalRing.ResidueField R)) ≤
      LinearMap.range ((LinearMap.ker f).subtype.baseChange (IsLocalRing.ResidueField R))) :
    Module.Free R (N ⧸ LinearMap.range f)

theorem

free_quotient_range_of_ker_baseChange_residueField_le

L73 ↗

Module.free_quotient_range_of_ker_baseChange_residueField_le

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_free_quotient_range_of_ker_baseChange_residueField_le
open scoped TensorProduct
universe u v w

Lean source · statement

theorem _root_.Module.free_quotient_range_of_ker_baseChange_residueField_le
    {R : Type u} [CommRing R] [IsLocalRing R]
    {M : Type v} {N : Type w} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
    [Module.Finite R M] [Module.Finite R N] [Module.Free R N] (f : M →ₗ[R] N)
    (h : LinearMap.ker (f.baseChange (IsLocalRing.ResidueField R)) ≤
      LinearMap.range ((LinearMap.ker f).subtype.baseChange (IsLocalRing.ResidueField R))) :
    Module.Free R (N ⧸ LinearMap.range f)

Module documentation

Module free quotient range of ker base Change residue Field le

Declarations

rangeRestrict_comp_ker_subtype

subtype_comp_rangeRestrict

lTensor_subtype_range_injective

free_quotient_range

free_quotient_range_of_ker_baseChange_residueField_le