Module

AddMonoidHom_natCard_ker_comp_eq_mul_of_surjective.lean

Nyll.AlgebraicCurves.Foundations.Algebra.AddMonoidHom_natCard_ker_comp_eq_mul_of_surjective

7 declarations indexed from sourceView source ↗

Module documentation

Add Monoid Hom nat Card ker comp eq mul of surjective

Imports2

Mathlib.GroupTheory.Coset.Card
Mathlib.GroupTheory.QuotientGroup.Basic

Imported by1

Nyll.AlgebraicCurves.Foundations.Algebra.All

def

kerMap

L30 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddMonoidHom_natCard_ker_comp_eq_mul_of_surjective.P2mKerMul.kerMap

Documentation

The map from the kernel of a composite to the kernel of its second map.

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddMonoidHom_natCard_ker_comp_eq_mul_of_surjective
namespace P2mKerMul
variable {A B C : Type*} [AddGroup A] [AddGroup B] [AddGroup C]

Lean source · statement

def kerMap (f : A →+ B) (g : B →+ C) : (g.comp f).ker →+ g.ker

theorem

kerMap_apply

L36 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddMonoidHom_natCard_ker_comp_eq_mul_of_surjective.P2mKerMul.kerMap_apply

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddMonoidHom_natCard_ker_comp_eq_mul_of_surjective
namespace P2mKerMul
variable {A B C : Type*} [AddGroup A] [AddGroup B] [AddGroup C]

Lean source · statement

theorem kerMap_apply (f : A →+ B) (g : B →+ C) (x : (g.comp f).ker) :
    (kerMap f g x : B) = f x

theorem

kerMap_surjective

L39 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddMonoidHom_natCard_ker_comp_eq_mul_of_surjective.P2mKerMul.kerMap_surjective

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddMonoidHom_natCard_ker_comp_eq_mul_of_surjective
namespace P2mKerMul
variable {A B C : Type*} [AddGroup A] [AddGroup B] [AddGroup C]

Lean source · statement

theorem kerMap_surjective (f : A →+ B) (g : B →+ C) (hf : Function.Surjective f) :
    Function.Surjective (kerMap f g)

theorem

ker_le

L48 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddMonoidHom_natCard_ker_comp_eq_mul_of_surjective.P2mKerMul.ker_le

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddMonoidHom_natCard_ker_comp_eq_mul_of_surjective
namespace P2mKerMul
variable {A B C : Type*} [AddGroup A] [AddGroup B] [AddGroup C]

Lean source · statement

theorem ker_le (f : A →+ B) (g : B →+ C) : f.ker ≤ (g.comp f).ker

theorem

ker_kerMap

L53 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddMonoidHom_natCard_ker_comp_eq_mul_of_surjective.P2mKerMul.ker_kerMap

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddMonoidHom_natCard_ker_comp_eq_mul_of_surjective
namespace P2mKerMul
variable {A B C : Type*} [AddGroup A] [AddGroup B] [AddGroup C]

Lean source · statement

theorem ker_kerMap (f : A →+ B) (g : B →+ C) :
    (kerMap f g).ker = f.ker.addSubgroupOf (g.comp f).ker

theorem

natCard_ker_comp

L60 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddMonoidHom_natCard_ker_comp_eq_mul_of_surjective.P2mKerMul.natCard_ker_comp

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddMonoidHom_natCard_ker_comp_eq_mul_of_surjective
namespace P2mKerMul
variable {A B C : Type*} [AddGroup A] [AddGroup B] [AddGroup C]

Lean source · statement

theorem natCard_ker_comp (f : A →+ B) (g : B →+ C) (hf : Function.Surjective f) :
    Nat.card (g.comp f).ker = Nat.card g.ker * Nat.card f.ker

theorem

natCard_ker_comp_eq_mul_of_surjective

L72 ↗

AddMonoidHom.natCard_ker_comp_eq_mul_of_surjective

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddMonoidHom_natCard_ker_comp_eq_mul_of_surjective

Lean source · statement

theorem _root_.AddMonoidHom.natCard_ker_comp_eq_mul_of_surjective {A B C : Type*} [AddGroup A]
  [AddGroup B] [AddGroup C]
    (f : A →+ B) (g : B →+ C) (hf : Function.Surjective f) :
    Nat.card (g.comp f).ker = Nat.card g.ker * Nat.card f.ker

Module documentation

Add Monoid Hom nat Card ker comp eq mul of surjective

Declarations

kerMap

kerMap_apply

kerMap_surjective

ker_le

ker_kerMap

natCard_ker_comp

natCard_ker_comp_eq_mul_of_surjective