add module homomorphisms and miscellany
This commit is contained in:
Jeremy Avigad
parent
4c713e921d
commit
153c8499af
2 changed files with 181 additions and 4 deletions
|
|
@ -7,8 +7,10 @@ Modules prod vector spaces over a ring.
|
|||
|
||||
(We use "left_module," which is more precise, because "module" is a keyword.)
|
||||
-/
|
||||
import algebra.field
|
||||
open algebra
|
||||
import algebra.field ..move_to_lib
|
||||
open is_trunc pointed function sigma eq
|
||||
|
||||
namespace algebra
|
||||
|
||||
structure has_scalar [class] (F V : Type) :=
|
||||
(smul : F → V → V)
|
||||
|
|
@ -84,3 +86,139 @@ end left_module
|
|||
|
||||
structure vector_space [class] (F V : Type) [fieldF : field F]
|
||||
extends left_module F V
|
||||
|
||||
/- homomorphisms -/
|
||||
|
||||
definition is_smul_hom [class] (R : Type) {M₁ M₂ : Type} [has_scalar R M₁] [has_scalar R M₂]
|
||||
(f : M₁ → M₂) : Type :=
|
||||
∀ r : R, ∀ a : M₁, f (r • a) = r • f a
|
||||
|
||||
definition is_prop_is_smul_hom [instance] (R : Type) {M₁ M₂ : Type} [is_set M₂]
|
||||
[has_scalar R M₁] [has_scalar R M₂] (f : M₁ → M₂) : is_prop (is_smul_hom R f) :=
|
||||
begin unfold is_smul_hom, apply _ end
|
||||
|
||||
definition respect_smul (R : Type) {M₁ M₂ : Type} [has_scalar R M₁] [has_scalar R M₂]
|
||||
(f : M₁ → M₂) [H : is_smul_hom R f] :
|
||||
∀ r : R, ∀ a : M₁, f (r • a) = r • f a :=
|
||||
H
|
||||
|
||||
definition is_module_hom [class] (R : Type) {M₁ M₂ : Type}
|
||||
[has_scalar R M₁] [has_scalar R M₂] [add_group M₁] [add_group M₂]
|
||||
(f : M₁ → M₂) :=
|
||||
is_add_hom f × is_smul_hom R f
|
||||
|
||||
definition is_add_hom_of_is_module_hom [instance] (R : Type) {M₁ M₂ : Type}
|
||||
[has_scalar R M₁] [has_scalar R M₂] [add_group M₁] [add_group M₂]
|
||||
(f : M₁ → M₂) [H : is_module_hom R f] : is_add_hom f :=
|
||||
prod.pr1 H
|
||||
|
||||
definition is_smul_hom_of_is_module_hom [instance] {R : Type} {M₁ M₂ : Type}
|
||||
[has_scalar R M₁] [has_scalar R M₂] [add_group M₁] [add_group M₂]
|
||||
(f : M₁ → M₂) [H : is_module_hom R f] : is_smul_hom R f :=
|
||||
prod.pr2 H
|
||||
|
||||
-- Why do we have to give the instance explicitly?
|
||||
definition is_prop_is_module_hom [instance] (R : Type) {M₁ M₂ : Type}
|
||||
[has_scalar R M₁] [has_scalar R M₂] [add_group M₁] [add_group M₂]
|
||||
(f : M₁ → M₂) : is_prop (is_module_hom R f) :=
|
||||
have h₁ : is_prop (is_add_hom f), from is_prop_is_add_hom f,
|
||||
begin unfold is_module_hom, apply _ end
|
||||
|
||||
section module_hom
|
||||
variables {R : Type} {M₁ M₂ M₃ : Type}
|
||||
variables [has_scalar R M₁] [has_scalar R M₂] [has_scalar R M₃]
|
||||
variables [add_group M₁] [add_group M₂] [add_group M₃]
|
||||
variables (g : M₂ → M₃) (f : M₁ → M₂) [is_module_hom R g] [is_module_hom R f]
|
||||
|
||||
proposition is_module_hom_id : is_module_hom R (@id M₁) :=
|
||||
pair (λ a₁ a₂, rfl) (λ r a, rfl)
|
||||
|
||||
proposition is_module_hom_comp : is_module_hom R (g ∘ f) :=
|
||||
pair
|
||||
(take a₁ a₂, begin esimp, rewrite [respect_add f, respect_add g] end)
|
||||
(take r a, by esimp; rewrite [respect_smul R f, respect_smul R g])
|
||||
|
||||
proposition respect_smul_add_smul (a b : R) (u v : M₁) : f (a • u + b • v) = a • f u + b • f v :=
|
||||
by rewrite [respect_add f, +respect_smul R f]
|
||||
end module_hom
|
||||
|
||||
structure LeftModule (R : Ring) :=
|
||||
(carrier : Type) (struct : left_module R carrier)
|
||||
|
||||
local attribute LeftModule.carrier [coercion]
|
||||
attribute LeftModule.struct [instance]
|
||||
|
||||
definition pointed_LeftModule_carrier [instance] {R : Ring} (M : LeftModule R) :
|
||||
pointed (LeftModule.carrier M) :=
|
||||
pointed.mk zero
|
||||
|
||||
definition pSet_of_LeftModule [coercion] {R : Ring} (M : LeftModule R) : Set* :=
|
||||
pSet.mk' (LeftModule.carrier M)
|
||||
|
||||
namespace left_module
|
||||
variable {R : Ring}
|
||||
|
||||
structure homomorphism (M₁ M₂ : LeftModule R) : Type :=
|
||||
(fn : LeftModule.carrier M₁ → LeftModule.carrier M₂)
|
||||
(p : is_module_hom R fn)
|
||||
|
||||
infix ` →lm `:55 := homomorphism
|
||||
|
||||
definition homomorphism_fn [unfold 4] [coercion] := @homomorphism.fn
|
||||
|
||||
definition is_module_hom_of_homomorphism [unfold 4] [instance] [priority 900]
|
||||
{M₁ M₂ : LeftModule R} (φ : M₁ →lm M₂) : is_module_hom R φ :=
|
||||
homomorphism.p φ
|
||||
|
||||
section
|
||||
variables {M₁ M₂ : LeftModule R} (φ : M₁ →lm M₂)
|
||||
|
||||
definition to_respect_add (x y : M₁) : φ (x + y) = φ x + φ y :=
|
||||
respect_add φ x y
|
||||
|
||||
definition to_respect_smul (a : R) (x : M₁) : φ (a • x) = a • (φ x) :=
|
||||
respect_smul R φ a x
|
||||
|
||||
definition is_embedding_of_homomorphism /- φ -/ (H : Π{x}, φ x = 0 → x = 0) : is_embedding φ :=
|
||||
is_embedding_of_is_add_hom φ @H
|
||||
|
||||
variables (M₁ M₂)
|
||||
definition is_set_homomorphism [instance] : is_set (M₁ →lm M₂) :=
|
||||
begin
|
||||
have H : M₁ →lm M₂ ≃ Σ(f : LeftModule.carrier M₁ → LeftModule.carrier M₂),
|
||||
is_module_hom (Ring.carrier R) f,
|
||||
begin
|
||||
fapply equiv.MK,
|
||||
{ intro φ, induction φ, constructor, exact p},
|
||||
{ intro v, induction v with f H, constructor, exact H},
|
||||
{ intro v, induction v, reflexivity},
|
||||
{ intro φ, induction φ, reflexivity}
|
||||
end,
|
||||
have ∀ f : LeftModule.carrier M₁ → LeftModule.carrier M₂,
|
||||
is_set (is_module_hom (Ring.carrier R) f), from _,
|
||||
apply is_trunc_equiv_closed_rev, exact H
|
||||
end
|
||||
|
||||
variables {M₁ M₂}
|
||||
definition pmap_of_homomorphism [constructor] /- φ -/ :
|
||||
pSet_of_LeftModule M₁ →* pSet_of_LeftModule M₂ :=
|
||||
have H : φ 0 = 0, from respect_zero φ,
|
||||
pmap.mk φ begin esimp, exact H end
|
||||
|
||||
definition homomorphism_change_fun [constructor]
|
||||
(φ : M₁ →lm M₂) (f : M₁ → M₂) (p : φ ~ f) : M₁ →lm M₂ :=
|
||||
homomorphism.mk f
|
||||
(prod.mk
|
||||
(λx₁ x₂, (p (x₁ + x₂))⁻¹ ⬝ to_respect_add φ x₁ x₂ ⬝ ap011 _ (p x₁) (p x₂))
|
||||
(λ a x, (p (a • x))⁻¹ ⬝ to_respect_smul φ a x ⬝ ap01 _ (p x)))
|
||||
|
||||
definition homomorphism_eq (φ₁ φ₂ : M₁ →lm M₂) (p : φ₁ ~ φ₂) : φ₁ = φ₂ :=
|
||||
begin
|
||||
induction φ₁ with φ₁ q₁, induction φ₂ with φ₂ q₂, esimp at p, induction p,
|
||||
exact ap (homomorphism.mk φ₂) !is_prop.elim
|
||||
end
|
||||
end
|
||||
|
||||
end left_module
|
||||
|
||||
end algebra
|
||||
|
|
|
|||
|
|
@ -968,14 +968,14 @@ begin
|
|||
exact ⦃ab_group, struct, mul_comm := H⦄
|
||||
end
|
||||
|
||||
definition trivial_ab_group : AbGroup.{0} :=
|
||||
definition trivial_ab_group : AbGroup.{0} :=
|
||||
begin
|
||||
fapply AbGroup_of_Group Trivial_group, intro x y, reflexivity
|
||||
end
|
||||
|
||||
definition trivial_homomorphism (A B : AbGroup) : A →g B :=
|
||||
begin
|
||||
fapply homomorphism.mk,
|
||||
fapply homomorphism.mk,
|
||||
exact λ a, 1,
|
||||
intros, symmetry, exact one_mul 1,
|
||||
end
|
||||
|
|
@ -992,3 +992,42 @@ definition is_embedding_from_trivial_ab_group (A : AbGroup) : is_embedding (from
|
|||
|
||||
definition to_trivial_ab_group (A : AbGroup) : A →g trivial_ab_group :=
|
||||
trivial_homomorphism A trivial_ab_group
|
||||
|
||||
/- Stuff added by Jeremy -/
|
||||
|
||||
definition exists.elim {A : Type} {p : A → Type} {B : Type} [is_prop B] (H : Exists p)
|
||||
(H' : ∀ (a : A), p a → B) : B :=
|
||||
trunc.elim (sigma.rec H') H
|
||||
|
||||
definition image.elim {A B : Type} {f : A → B} {C : Type} [is_prop C] {b : B}
|
||||
(H : image f b) (H' : ∀ (a : A), f a = b → C) : C :=
|
||||
begin
|
||||
refine (trunc.elim _ H),
|
||||
intro H'', cases H'' with a Ha, exact H' a Ha
|
||||
end
|
||||
|
||||
definition image.intro {A B : Type} {f : A → B} {a : A} {b : B} (h : f a = b) : image f b :=
|
||||
begin
|
||||
apply trunc.merely.intro,
|
||||
apply fiber.mk,
|
||||
exact h
|
||||
end
|
||||
|
||||
definition image.equiv_exists {A B : Type} {f : A → B} {b : B} : image f b ≃ ∃ a, f a = b :=
|
||||
trunc_equiv_trunc _ (fiber.sigma_char _ _)
|
||||
|
||||
-- move to homomorphism.hlean
|
||||
section
|
||||
theorem eq_zero_of_eq_zero_of_is_embedding {A B : Type} [add_group A] [add_group B]
|
||||
{f : A → B} [is_add_hom f] [is_embedding f] {a : A} (h : f a = 0) : a = 0 :=
|
||||
have f a = f 0, by rewrite [h, respect_zero],
|
||||
show a = 0, from is_injective_of_is_embedding this
|
||||
end
|
||||
|
||||
/- put somewhere in algebra -/
|
||||
|
||||
structure Ring :=
|
||||
(carrier : Type) (struct : ring carrier)
|
||||
|
||||
attribute Ring.carrier [coercion]
|
||||
attribute Ring.struct [instance]
|
||||
|
|
|
|||
Loading…
Reference in a new issue