map and comap for Submodules #
Main declarations #
Submodule.map: The pushforward of a submodulep ⊆ Mbyf : M → M₂Submodule.comap: The pullback of a submodulep ⊆ M₂alongf : M → M₂Submodule.giMapComap:map fandcomap fform aGaloisInsertionwhenfis surjective.Submodule.gciMapComap:map fandcomap fform aGaloisCoinsertionwhenfis injective.
Tags #
submodule, subspace, linear map, pushforward, pullback
def
Submodule.map
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
(p : Submodule R M)
:
Submodule R₂ M₂
The pushforward of a submodule p ⊆ M by f : M → M₂
Equations
- Submodule.map f p = let __src := AddSubmonoid.map f p.toAddSubmonoid; { carrier := ⇑f '' ↑p, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
@[simp]
theorem
Submodule.map_coe
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
(p : Submodule R M)
:
↑(Submodule.map f p) = ⇑f '' ↑p
theorem
Submodule.map_toAddSubmonoid
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
(f : M →ₛₗ[σ₁₂] M₂)
(p : Submodule R M)
:
(Submodule.map f p).toAddSubmonoid = AddSubmonoid.map (↑f) p.toAddSubmonoid
theorem
Submodule.map_toAddSubmonoid'
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
(f : M →ₛₗ[σ₁₂] M₂)
(p : Submodule R M)
:
(Submodule.map f p).toAddSubmonoid = AddSubmonoid.map f p.toAddSubmonoid
@[simp]
theorem
AddMonoidHom.coe_toIntLinearMap_map
{A : Type u_10}
{A₂ : Type u_11}
[AddCommGroup A]
[AddCommGroup A₂]
(f : A →+ A₂)
(s : AddSubgroup A)
:
Submodule.map f.toIntLinearMap (AddSubgroup.toIntSubmodule s) = AddSubgroup.toIntSubmodule (AddSubgroup.map f s)
@[simp]
theorem
MonoidHom.coe_toAdditive_map
{G : Type u_10}
{G₂ : Type u_11}
[Group G]
[Group G₂]
(f : G →* G₂)
(s : Subgroup G)
:
AddSubgroup.map (MonoidHom.toAdditive f) (Subgroup.toAddSubgroup s) = Subgroup.toAddSubgroup (Subgroup.map f s)
@[simp]
theorem
AddMonoidHom.coe_toMultiplicative_map
{G : Type u_10}
{G₂ : Type u_11}
[AddGroup G]
[AddGroup G₂]
(f : G →+ G₂)
(s : AddSubgroup G)
:
Subgroup.map (AddMonoidHom.toMultiplicative f) (AddSubgroup.toSubgroup s) = AddSubgroup.toSubgroup (AddSubgroup.map f s)
@[simp]
theorem
Submodule.mem_map
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{f : F}
{p : Submodule R M}
{x : M₂}
:
x ∈ Submodule.map f p ↔ ∃ y ∈ p, f y = x
theorem
Submodule.mem_map_of_mem
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{f : F}
{p : Submodule R M}
{r : M}
(h : r ∈ p)
:
f r ∈ Submodule.map f p
theorem
Submodule.apply_coe_mem_map
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
{p : Submodule R M}
(r : ↥p)
:
f ↑r ∈ Submodule.map f p
@[simp]
theorem
Submodule.map_id
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
:
Submodule.map LinearMap.id p = p
theorem
Submodule.map_comp
{R : Type u_1}
{R₂ : Type u_3}
{R₃ : Type u_4}
{M : Type u_5}
{M₂ : Type u_7}
{M₃ : Type u_8}
[Semiring R]
[Semiring R₂]
[Semiring R₃]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R₂ M₂]
[Module R₃ M₃]
{σ₁₂ : R →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[RingHomSurjective σ₁₂]
[RingHomSurjective σ₂₃]
[RingHomSurjective σ₁₃]
(f : M →ₛₗ[σ₁₂] M₂)
(g : M₂ →ₛₗ[σ₂₃] M₃)
(p : Submodule R M)
:
Submodule.map (g.comp f) p = Submodule.map g (Submodule.map f p)
theorem
Submodule.map_mono
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{f : F}
{p : Submodule R M}
{p' : Submodule R M}
:
p ≤ p' → Submodule.map f p ≤ Submodule.map f p'
@[simp]
theorem
Submodule.map_zero
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
(p : Submodule R M)
[RingHomSurjective σ₁₂]
:
Submodule.map 0 p = ⊥
theorem
Submodule.map_add_le
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
(p : Submodule R M)
[RingHomSurjective σ₁₂]
(f : M →ₛₗ[σ₁₂] M₂)
(g : M →ₛₗ[σ₁₂] M₂)
:
Submodule.map (f + g) p ≤ Submodule.map f p ⊔ Submodule.map g p
theorem
Submodule.map_inf_le
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
{p : Submodule R M}
{q : Submodule R M}
:
Submodule.map f (p ⊓ q) ≤ Submodule.map f p ⊓ Submodule.map f q
theorem
Submodule.map_inf
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
{p : Submodule R M}
{q : Submodule R M}
(hf : Function.Injective ⇑f)
:
Submodule.map f (p ⊓ q) = Submodule.map f p ⊓ Submodule.map f q
theorem
Submodule.range_map_nonempty
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
(N : Submodule R M)
:
(Set.range fun (ϕ : M →ₛₗ[σ₁₂] M₂) => Submodule.map ϕ N).Nonempty
noncomputable def
Submodule.equivMapOfInjective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
(i : Function.Injective ⇑f)
(p : Submodule R M)
:
↥p ≃ₛₗ[σ₁₂] ↥(Submodule.map f p)
The pushforward of a submodule by an injective linear map is
linearly equivalent to the original submodule. See also LinearEquiv.submoduleMap for a
computable version when f has an explicit inverse.
Equations
- Submodule.equivMapOfInjective f i p = let __src := Equiv.Set.image (⇑f) (↑p) i; { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }
Instances For
@[simp]
theorem
Submodule.coe_equivMapOfInjective_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
(i : Function.Injective ⇑f)
(p : Submodule R M)
(x : ↥p)
:
↑((Submodule.equivMapOfInjective f i p) x) = f ↑x
@[simp]
theorem
Submodule.map_equivMapOfInjective_symm_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
(i : Function.Injective ⇑f)
(p : Submodule R M)
(x : ↥(Submodule.map f p))
:
f ↑((Submodule.equivMapOfInjective f i p).symm x) = ↑x
def
Submodule.comap
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
(p : Submodule R₂ M₂)
:
Submodule R M
The pullback of a submodule p ⊆ M₂ along f : M → M₂
Equations
- Submodule.comap f p = let __src := AddSubmonoid.comap f p.toAddSubmonoid; { carrier := ⇑f ⁻¹' ↑p, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
@[simp]
theorem
Submodule.comap_coe
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
(p : Submodule R₂ M₂)
:
↑(Submodule.comap f p) = ⇑f ⁻¹' ↑p
@[simp]
theorem
Submodule.AddMonoidHom.coe_toIntLinearMap_comap
{A : Type u_10}
{A₂ : Type u_11}
[AddCommGroup A]
[AddCommGroup A₂]
(f : A →+ A₂)
(s : AddSubgroup A₂)
:
Submodule.comap f.toIntLinearMap (AddSubgroup.toIntSubmodule s) = AddSubgroup.toIntSubmodule (AddSubgroup.comap f s)
@[simp]
theorem
Submodule.mem_comap
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{x : M}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{f : F}
{p : Submodule R₂ M₂}
:
x ∈ Submodule.comap f p ↔ f x ∈ p
@[simp]
theorem
Submodule.comap_id
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
:
Submodule.comap LinearMap.id p = p
theorem
Submodule.comap_comp
{R : Type u_1}
{R₂ : Type u_3}
{R₃ : Type u_4}
{M : Type u_5}
{M₂ : Type u_7}
{M₃ : Type u_8}
[Semiring R]
[Semiring R₂]
[Semiring R₃]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R₂ M₂]
[Module R₃ M₃]
{σ₁₂ : R →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
(f : M →ₛₗ[σ₁₂] M₂)
(g : M₂ →ₛₗ[σ₂₃] M₃)
(p : Submodule R₃ M₃)
:
Submodule.comap (g.comp f) p = Submodule.comap f (Submodule.comap g p)
theorem
Submodule.comap_mono
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{f : F}
{q : Submodule R₂ M₂}
{q' : Submodule R₂ M₂}
:
q ≤ q' → Submodule.comap f q ≤ Submodule.comap f q'
theorem
Submodule.le_comap_pow_of_le_comap
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
{f : M →ₗ[R] M}
(h : p ≤ Submodule.comap f p)
(k : ℕ)
:
p ≤ Submodule.comap (f ^ k) p
theorem
Submodule.map_le_iff_le_comap
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
{f : F}
{p : Submodule R M}
{q : Submodule R₂ M₂}
:
Submodule.map f p ≤ q ↔ p ≤ Submodule.comap f q
theorem
Submodule.gc_map_comap
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
(f : F)
:
@[simp]
theorem
Submodule.map_bot
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
(f : F)
:
Submodule.map f ⊥ = ⊥
@[simp]
theorem
Submodule.map_sup
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
(p : Submodule R M)
(p' : Submodule R M)
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
(f : F)
:
Submodule.map f (p ⊔ p') = Submodule.map f p ⊔ Submodule.map f p'
@[simp]
theorem
Submodule.map_iSup
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
{ι : Sort u_10}
(f : F)
(p : ι → Submodule R M)
:
Submodule.map f (⨆ (i : ι), p i) = ⨆ (i : ι), Submodule.map f (p i)
@[simp]
theorem
Submodule.comap_top
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
:
Submodule.comap f ⊤ = ⊤
@[simp]
theorem
Submodule.comap_inf
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
(q : Submodule R₂ M₂)
(q' : Submodule R₂ M₂)
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
:
Submodule.comap f (q ⊓ q') = Submodule.comap f q ⊓ Submodule.comap f q'
@[simp]
theorem
Submodule.comap_iInf
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
{ι : Sort u_10}
(f : F)
(p : ι → Submodule R₂ M₂)
:
Submodule.comap f (⨅ (i : ι), p i) = ⨅ (i : ι), Submodule.comap f (p i)
@[simp]
theorem
Submodule.comap_zero
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
(q : Submodule R₂ M₂)
:
Submodule.comap 0 q = ⊤
theorem
Submodule.map_comap_le
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
(f : F)
(q : Submodule R₂ M₂)
:
Submodule.map f (Submodule.comap f q) ≤ q
theorem
Submodule.le_comap_map
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
(f : F)
(p : Submodule R M)
:
p ≤ Submodule.comap f (Submodule.map f p)
def
Submodule.giMapComap
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{f : F}
(hf : Function.Surjective ⇑f)
[RingHomSurjective σ₁₂]
:
map f and comap f form a GaloisInsertion when f is surjective.
Equations
- Submodule.giMapComap hf = ⋯.toGaloisInsertion ⋯
Instances For
theorem
Submodule.map_comap_eq_of_surjective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{f : F}
(hf : Function.Surjective ⇑f)
[RingHomSurjective σ₁₂]
(p : Submodule R₂ M₂)
:
Submodule.map f (Submodule.comap f p) = p
theorem
Submodule.map_surjective_of_surjective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{f : F}
(hf : Function.Surjective ⇑f)
[RingHomSurjective σ₁₂]
:
theorem
Submodule.comap_injective_of_surjective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{f : F}
(hf : Function.Surjective ⇑f)
[RingHomSurjective σ₁₂]
:
theorem
Submodule.map_sup_comap_of_surjective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{f : F}
(hf : Function.Surjective ⇑f)
[RingHomSurjective σ₁₂]
(p : Submodule R₂ M₂)
(q : Submodule R₂ M₂)
:
Submodule.map f (Submodule.comap f p ⊔ Submodule.comap f q) = p ⊔ q
theorem
Submodule.map_iSup_comap_of_sujective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{f : F}
(hf : Function.Surjective ⇑f)
[RingHomSurjective σ₁₂]
{ι : Sort u_10}
(S : ι → Submodule R₂ M₂)
:
Submodule.map f (⨆ (i : ι), Submodule.comap f (S i)) = iSup S
theorem
Submodule.map_inf_comap_of_surjective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{f : F}
(hf : Function.Surjective ⇑f)
[RingHomSurjective σ₁₂]
(p : Submodule R₂ M₂)
(q : Submodule R₂ M₂)
:
Submodule.map f (Submodule.comap f p ⊓ Submodule.comap f q) = p ⊓ q
theorem
Submodule.map_iInf_comap_of_surjective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{f : F}
(hf : Function.Surjective ⇑f)
[RingHomSurjective σ₁₂]
{ι : Sort u_10}
(S : ι → Submodule R₂ M₂)
:
Submodule.map f (⨅ (i : ι), Submodule.comap f (S i)) = iInf S
theorem
Submodule.comap_le_comap_iff_of_surjective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{f : F}
(hf : Function.Surjective ⇑f)
[RingHomSurjective σ₁₂]
(p : Submodule R₂ M₂)
(q : Submodule R₂ M₂)
:
Submodule.comap f p ≤ Submodule.comap f q ↔ p ≤ q
theorem
Submodule.comap_strictMono_of_surjective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{f : F}
(hf : Function.Surjective ⇑f)
[RingHomSurjective σ₁₂]
:
def
Submodule.gciMapComap
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
{f : F}
(hf : Function.Injective ⇑f)
:
map f and comap f form a GaloisCoinsertion when f is injective.
Equations
- Submodule.gciMapComap hf = ⋯.toGaloisCoinsertion ⋯
Instances For
theorem
Submodule.comap_map_eq_of_injective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
{f : F}
(hf : Function.Injective ⇑f)
(p : Submodule R M)
:
Submodule.comap f (Submodule.map f p) = p
theorem
Submodule.comap_surjective_of_injective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
{f : F}
(hf : Function.Injective ⇑f)
:
theorem
Submodule.map_injective_of_injective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
{f : F}
(hf : Function.Injective ⇑f)
:
theorem
Submodule.comap_inf_map_of_injective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
{f : F}
(hf : Function.Injective ⇑f)
(p : Submodule R M)
(q : Submodule R M)
:
Submodule.comap f (Submodule.map f p ⊓ Submodule.map f q) = p ⊓ q
theorem
Submodule.comap_iInf_map_of_injective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
{f : F}
(hf : Function.Injective ⇑f)
{ι : Sort u_10}
(S : ι → Submodule R M)
:
Submodule.comap f (⨅ (i : ι), Submodule.map f (S i)) = iInf S
theorem
Submodule.comap_sup_map_of_injective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
{f : F}
(hf : Function.Injective ⇑f)
(p : Submodule R M)
(q : Submodule R M)
:
Submodule.comap f (Submodule.map f p ⊔ Submodule.map f q) = p ⊔ q
theorem
Submodule.comap_iSup_map_of_injective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
{f : F}
(hf : Function.Injective ⇑f)
{ι : Sort u_10}
(S : ι → Submodule R M)
:
Submodule.comap f (⨆ (i : ι), Submodule.map f (S i)) = iSup S
theorem
Submodule.map_le_map_iff_of_injective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
{f : F}
(hf : Function.Injective ⇑f)
(p : Submodule R M)
(q : Submodule R M)
:
Submodule.map f p ≤ Submodule.map f q ↔ p ≤ q
theorem
Submodule.map_strictMono_of_injective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
{f : F}
(hf : Function.Injective ⇑f)
:
@[simp]
theorem
Submodule.orderIsoMapComapOfBijective_symm_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
(hf : Function.Bijective ⇑f)
(p : Submodule R₂ M₂)
:
(RelIso.symm (Submodule.orderIsoMapComapOfBijective f hf)) p = Submodule.comap f p
@[simp]
theorem
Submodule.orderIsoMapComapOfBijective_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
(hf : Function.Bijective ⇑f)
(p : Submodule R M)
:
(Submodule.orderIsoMapComapOfBijective f hf) p = Submodule.map f p
def
Submodule.orderIsoMapComapOfBijective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
(hf : Function.Bijective ⇑f)
:
A linear isomorphism induces an order isomorphism of submodules.
Equations
- Submodule.orderIsoMapComapOfBijective f hf = { toFun := Submodule.map f, invFun := Submodule.comap f, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
Instances For
@[simp]
theorem
Submodule.orderIsoMapComap_symm_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_9}
[EquivLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
(p : Submodule R₂ M₂)
:
(RelIso.symm (Submodule.orderIsoMapComap f)) p = Submodule.comap f p
@[simp]
theorem
Submodule.orderIsoMapComap_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_9}
[EquivLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
(p : Submodule R M)
:
(Submodule.orderIsoMapComap f) p = Submodule.map f p
def
Submodule.orderIsoMapComap
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_9}
[EquivLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
:
A linear isomorphism induces an order isomorphism of submodules.
Equations
Instances For
theorem
Submodule.map_inf_eq_map_inf_comap
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_9}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
{f : F}
{p : Submodule R M}
{p' : Submodule R₂ M₂}
:
Submodule.map f p ⊓ p' = Submodule.map f (p ⊓ Submodule.comap f p')
@[simp]
theorem
Submodule.map_comap_subtype
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
(p' : Submodule R M)
:
Submodule.map p.subtype (Submodule.comap p.subtype p') = p ⊓ p'
theorem
Submodule.eq_zero_of_bot_submodule
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(b : ↥⊥)
:
b = 0
theorem
LinearMap.iInf_invariant
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{σ : R →+* R}
[RingHomSurjective σ]
{ι : Sort u_10}
(f : M →ₛₗ[σ] M)
{p : ι → Submodule R M}
(hf : ∀ (i : ι), ∀ v ∈ p i, f v ∈ p i)
(v : M)
:
The infimum of a family of invariant submodule of an endomorphism is also an invariant submodule.
theorem
Submodule.disjoint_iff_comap_eq_bot
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{p : Submodule R M}
{q : Submodule R M}
:
Disjoint p q ↔ Submodule.comap p.subtype q = ⊥
@[simp]
theorem
Submodule.map_neg
{R : Type u_1}
{M : Type u_5}
{M₂ : Type u_7}
[Ring R]
[AddCommGroup M]
[Module R M]
(p : Submodule R M)
[AddCommGroup M₂]
[Module R M₂]
(f : M →ₗ[R] M₂)
:
Submodule.map (-f) p = Submodule.map f p
@[simp]
theorem
Submodule.comap_neg
{R : Type u_1}
{M : Type u_5}
{M₂ : Type u_7}
[Ring R]
[AddCommGroup M]
[Module R M]
[AddCommGroup M₂]
[Module R M₂]
{f : M →ₗ[R] M₂}
{p : Submodule R M₂}
:
Submodule.comap (-f) p = Submodule.comap f p
theorem
Submodule.comap_smul
{K : Type u_9}
{V : Type u_10}
{V₂ : Type u_11}
[Semifield K]
[AddCommMonoid V]
[Module K V]
[AddCommMonoid V₂]
[Module K V₂]
(f : V →ₗ[K] V₂)
(p : Submodule K V₂)
(a : K)
(h : a ≠ 0)
:
Submodule.comap (a • f) p = Submodule.comap f p
theorem
Submodule.map_smul
{K : Type u_9}
{V : Type u_10}
{V₂ : Type u_11}
[Semifield K]
[AddCommMonoid V]
[Module K V]
[AddCommMonoid V₂]
[Module K V₂]
(f : V →ₗ[K] V₂)
(p : Submodule K V)
(a : K)
(h : a ≠ 0)
:
Submodule.map (a • f) p = Submodule.map f p
theorem
Submodule.comap_smul'
{K : Type u_9}
{V : Type u_10}
{V₂ : Type u_11}
[Semifield K]
[AddCommMonoid V]
[Module K V]
[AddCommMonoid V₂]
[Module K V₂]
(f : V →ₗ[K] V₂)
(p : Submodule K V₂)
(a : K)
:
Submodule.comap (a • f) p = ⨅ (_ : a ≠ 0), Submodule.comap f p
theorem
Submodule.map_smul'
{K : Type u_9}
{V : Type u_10}
{V₂ : Type u_11}
[Semifield K]
[AddCommMonoid V]
[Module K V]
[AddCommMonoid V₂]
[Module K V₂]
(f : V →ₗ[K] V₂)
(p : Submodule K V)
(a : K)
:
Submodule.map (a • f) p = ⨆ (_ : a ≠ 0), Submodule.map f p
@[simp]
theorem
Submodule.comapSubtypeEquivOfLe_symm_apply
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{p : Submodule R M}
{q : Submodule R M}
(hpq : p ≤ q)
(x : ↥p)
:
(Submodule.comapSubtypeEquivOfLe hpq).symm x = ⟨⟨↑x, ⋯⟩, ⋯⟩
def
Submodule.comapSubtypeEquivOfLe
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{p : Submodule R M}
{q : Submodule R M}
(hpq : p ≤ q)
:
↥(Submodule.comap q.subtype p) ≃ₗ[R] ↥p
If s ≤ t, then we can view s as a submodule of t by taking the comap
of t.subtype.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Submodule.comapSubtypeEquivOfLe_apply_coe
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{p : Submodule R M}
{q : Submodule R M}
(hpq : p ≤ q)
(x : ↥(Submodule.comap q.subtype p))
:
↑((Submodule.comapSubtypeEquivOfLe hpq) x) = ↑↑x
@[simp]
theorem
Submodule.mem_map_equiv
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{τ₂₁ : R₂ →+* R}
[RingHomInvPair τ₁₂ τ₂₁]
[RingHomInvPair τ₂₁ τ₁₂]
(p : Submodule R M)
{e : M ≃ₛₗ[τ₁₂] M₂}
{x : M₂}
:
x ∈ Submodule.map (↑e) p ↔ e.symm x ∈ p
theorem
Submodule.map_equiv_eq_comap_symm
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{τ₂₁ : R₂ →+* R}
[RingHomInvPair τ₁₂ τ₂₁]
[RingHomInvPair τ₂₁ τ₁₂]
(e : M ≃ₛₗ[τ₁₂] M₂)
(K : Submodule R M)
:
Submodule.map (↑e) K = Submodule.comap (↑e.symm) K
theorem
Submodule.comap_equiv_eq_map_symm
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{τ₂₁ : R₂ →+* R}
[RingHomInvPair τ₁₂ τ₂₁]
[RingHomInvPair τ₂₁ τ₁₂]
(e : M ≃ₛₗ[τ₁₂] M₂)
(K : Submodule R₂ M₂)
:
Submodule.comap (↑e) K = Submodule.map (↑e.symm) K
theorem
Submodule.map_symm_eq_iff
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{τ₂₁ : R₂ →+* R}
[RingHomInvPair τ₁₂ τ₂₁]
[RingHomInvPair τ₂₁ τ₁₂]
{p : Submodule R M}
(e : M ≃ₛₗ[τ₁₂] M₂)
{K : Submodule R₂ M₂}
:
Submodule.map e.symm K = p ↔ Submodule.map e p = K
theorem
Submodule.orderIsoMapComap_apply'
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{τ₂₁ : R₂ →+* R}
[RingHomInvPair τ₁₂ τ₂₁]
[RingHomInvPair τ₂₁ τ₁₂]
(e : M ≃ₛₗ[τ₁₂] M₂)
(p : Submodule R M)
:
(Submodule.orderIsoMapComap e) p = Submodule.comap e.symm p
theorem
Submodule.orderIsoMapComap_symm_apply'
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{τ₂₁ : R₂ →+* R}
[RingHomInvPair τ₁₂ τ₂₁]
[RingHomInvPair τ₂₁ τ₁₂]
(e : M ≃ₛₗ[τ₁₂] M₂)
(p : Submodule R₂ M₂)
:
(Submodule.orderIsoMapComap e).symm p = Submodule.map e.symm p
theorem
Submodule.inf_comap_le_comap_add
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
(q : Submodule R₂ M₂)
(f₁ : M →ₛₗ[τ₁₂] M₂)
(f₂ : M →ₛₗ[τ₁₂] M₂)
:
Submodule.comap f₁ q ⊓ Submodule.comap f₂ q ≤ Submodule.comap (f₁ + f₂) q
theorem
Submodule.comap_le_comap_smul
{R : Type u_1}
{N : Type u_9}
{N₂ : Type u_10}
[CommSemiring R]
[AddCommMonoid N]
[AddCommMonoid N₂]
[Module R N]
[Module R N₂]
(qₗ : Submodule R N₂)
(fₗ : N →ₗ[R] N₂)
(c : R)
:
Submodule.comap fₗ qₗ ≤ Submodule.comap (c • fₗ) qₗ
def
Submodule.compatibleMaps
{R : Type u_1}
{N : Type u_9}
{N₂ : Type u_10}
[CommSemiring R]
[AddCommMonoid N]
[AddCommMonoid N₂]
[Module R N]
[Module R N₂]
(pₗ : Submodule R N)
(qₗ : Submodule R N₂)
:
Given modules M, M₂ over a commutative ring, together with submodules p ⊆ M, q ⊆ M₂,
the set of maps $\{f ∈ Hom(M, M₂) | f(p) ⊆ q \}$ is a submodule of Hom(M, M₂).
Equations
- pₗ.compatibleMaps qₗ = { carrier := {fₗ : N →ₗ[R] N₂ | pₗ ≤ Submodule.comap fₗ qₗ}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
def
LinearMap.submoduleMap
{R : Type u_1}
{M : Type u_5}
{M₁ : Type u_6}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₁]
[Module R M]
[Module R M₁]
(f : M →ₗ[R] M₁)
(p : Submodule R M)
:
↥p →ₗ[R] ↥(Submodule.map f p)
A linear map between two modules restricts to a linear map from any submodule p of the domain onto the image of that submodule.
This is the linear version of AddMonoidHom.addSubmonoidMap and AddMonoidHom.addSubgroupMap.
Equations
- f.submoduleMap p = f.restrict ⋯
Instances For
@[simp]
theorem
LinearMap.submoduleMap_coe_apply
{R : Type u_1}
{M : Type u_5}
{M₁ : Type u_6}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₁]
[Module R M]
[Module R M₁]
(f : M →ₗ[R] M₁)
{p : Submodule R M}
(x : ↥p)
:
↑((f.submoduleMap p) x) = f ↑x
theorem
LinearMap.submoduleMap_surjective
{R : Type u_1}
{M : Type u_5}
{M₁ : Type u_6}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₁]
[Module R M]
[Module R M₁]
(f : M →ₗ[R] M₁)
(p : Submodule R M)
:
Function.Surjective ⇑(f.submoduleMap p)
theorem
LinearMap.map_codRestrict
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{σ₂₁ : R₂ →+* R}
[RingHomSurjective σ₂₁]
(p : Submodule R M)
(f : M₂ →ₛₗ[σ₂₁] M)
(h : ∀ (c : M₂), f c ∈ p)
(p' : Submodule R₂ M₂)
:
Submodule.map (LinearMap.codRestrict p f h) p' = Submodule.comap p.subtype (Submodule.map f p')
theorem
LinearMap.comap_codRestrict
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{σ₂₁ : R₂ →+* R}
(p : Submodule R M)
(f : M₂ →ₛₗ[σ₂₁] M)
(hf : ∀ (c : M₂), f c ∈ p)
(p' : Submodule R ↥p)
:
Submodule.comap (LinearMap.codRestrict p f hf) p' = Submodule.comap f (Submodule.map p.subtype p')
Linear equivalences #
theorem
LinearEquiv.map_eq_comap
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{module_M : Module R M}
{module_M₂ : Module R₂ M₂}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
{re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
(e : M ≃ₛₗ[σ₁₂] M₂)
{p : Submodule R M}
:
Submodule.map (↑e) p = Submodule.comap (↑e.symm) p
def
LinearEquiv.submoduleMap
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{module_M : Module R M}
{module_M₂ : Module R₂ M₂}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
{re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
(e : M ≃ₛₗ[σ₁₂] M₂)
(p : Submodule R M)
:
↥p ≃ₛₗ[σ₁₂] ↥(Submodule.map (↑e) p)
A linear equivalence of two modules restricts to a linear equivalence from any submodule
p of the domain onto the image of that submodule.
This is the linear version of AddEquiv.submonoidMap and AddEquiv.subgroupMap.
This is LinearEquiv.ofSubmodule' but with map on the right instead of comap on the left.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LinearEquiv.submoduleMap_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{module_M : Module R M}
{module_M₂ : Module R₂ M₂}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
{re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
(e : M ≃ₛₗ[σ₁₂] M₂)
(p : Submodule R M)
(x : ↥p)
:
↑((e.submoduleMap p) x) = e ↑x
@[simp]
theorem
LinearEquiv.submoduleMap_symm_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_5}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{module_M : Module R M}
{module_M₂ : Module R₂ M₂}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
{re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
(e : M ≃ₛₗ[σ₁₂] M₂)
(p : Submodule R M)
(x : ↥(Submodule.map (↑e) p))
:
↑((e.submoduleMap p).symm x) = e.symm ↑x