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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_10}
[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
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Submodule.map_coe
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[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_6}
{M₂ : Type u_8}
[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_11}
{A₂ : Type u_12}
[AddCommGroup A]
[AddCommGroup A₂]
(f : A →+ A₂)
(s : AddSubgroup A)
:
Submodule.map (AddMonoidHom.toIntLinearMap f) (AddSubgroup.toIntSubmodule s) = AddSubgroup.toIntSubmodule (AddSubgroup.map f s)
@[simp]
theorem
MonoidHom.coe_toAdditive_map
{G : Type u_11}
{G₂ : Type u_12}
[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_11}
{G₂ : Type u_12}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_10}
[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_6}
[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_6}
{M₂ : Type u_8}
{M₃ : Type u_9}
[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 (LinearMap.comp g f) p = Submodule.map g (Submodule.map f p)
theorem
Submodule.map_mono
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[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_6}
{M₂ : Type u_8}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
[RingHomSurjective σ₁₂]
(N : Submodule R M)
:
Set.Nonempty (Set.range fun (ϕ : M →ₛₗ[σ₁₂] M₂) => Submodule.map ϕ N)
noncomputable def
Submodule.equivMapOfInjective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{F : Type u_10}
[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
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Submodule.coe_equivMapOfInjective_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
(i : Function.Injective ⇑f)
(p : Submodule R M)
(x : ↥(Submodule.map f p))
:
f ↑((LinearEquiv.symm (Submodule.equivMapOfInjective f i p)) x) = ↑x
def
Submodule.comap
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Submodule.comap_coe
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_11}
{A₂ : Type u_12}
[AddCommGroup A]
[AddCommGroup A₂]
(f : A →+ A₂)
(s : AddSubgroup A₂)
:
Submodule.comap (AddMonoidHom.toIntLinearMap f) (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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{x : M}
{F : Type u_10}
[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_6}
[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_6}
{M₂ : Type u_8}
{M₃ : Type u_9}
[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 (LinearMap.comp g f) p = Submodule.comap f (Submodule.comap g p)
theorem
Submodule.comap_mono
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_6}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[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_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
{ι : Sort u_11}
(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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[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_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
{ι : Sort u_11}
(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_6}
{M₂ : Type u_8}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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
- One or more equations did not get rendered due to their size.
Instances For
theorem
Submodule.map_comap_eq_of_surjective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{f : F}
(hf : Function.Surjective ⇑f)
[RingHomSurjective σ₁₂]
{ι : Sort u_11}
(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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{f : F}
(hf : Function.Surjective ⇑f)
[RingHomSurjective σ₁₂]
{ι : Sort u_11}
(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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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
- One or more equations did not get rendered due to their size.
Instances For
theorem
Submodule.comap_map_eq_of_injective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
{f : F}
(hf : Function.Injective ⇑f)
{ι : Sort u_11}
(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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
{f : F}
(hf : Function.Injective ⇑f)
{ι : Sort u_11}
(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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
{f : F}
(hf : Function.Injective ⇑f)
:
@[simp]
theorem
Submodule.orderIsoMapComap_symm_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{F : Type u_10}
[EquivLike F M M₂]
[SemilinearEquivClass 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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{F : Type u_10}
[EquivLike F M M₂]
[SemilinearEquivClass 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_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{F : Type u_10}
[EquivLike F M M₂]
[SemilinearEquivClass F σ₁₂ M M₂]
(f : F)
:
A linear isomorphism induces an order isomorphism of submodules.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Submodule.map_inf_eq_map_inf_comap
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_10}
[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')
theorem
Submodule.map_comap_subtype
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
(p' : Submodule R M)
:
Submodule.map (Submodule.subtype p) (Submodule.comap (Submodule.subtype p) p') = p ⊓ p'
theorem
Submodule.eq_zero_of_bot_submodule
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(b : ↥⊥)
:
b = 0
theorem
LinearMap.iInf_invariant
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{σ : R →+* R}
[RingHomSurjective σ]
{ι : Sort u_11}
(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.
@[simp]
theorem
Submodule.map_neg
{R : Type u_1}
{M : Type u_6}
{M₂ : Type u_8}
[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_6}
{M₂ : Type u_8}
[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_10}
{V : Type u_11}
{V₂ : Type u_12}
[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_10}
{V : Type u_11}
{V₂ : Type u_12}
[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_10}
{V : Type u_11}
{V₂ : Type u_12}
[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_10}
{V : Type u_11}
{V₂ : Type u_12}
[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_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{p : Submodule R M}
{q : Submodule R M}
(hpq : p ≤ q)
(x : ↥p)
:
(LinearEquiv.symm (Submodule.comapSubtypeEquivOfLe hpq)) x = { val := { val := ↑x, property := (_ : ↑x ∈ q) }, property := (_ : ↑x ∈ p) }
def
Submodule.comapSubtypeEquivOfLe
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{p : Submodule R M}
{q : Submodule R M}
(hpq : p ≤ q)
:
↥(Submodule.comap (Submodule.subtype q) 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_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{p : Submodule R M}
{q : Submodule R M}
(hpq : p ≤ q)
(x : ↥(Submodule.comap (Submodule.subtype q) p))
:
↑((Submodule.comapSubtypeEquivOfLe hpq) x) = ↑↑x
@[simp]
theorem
Submodule.mem_map_equiv
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[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 ↔ (LinearEquiv.symm e) x ∈ p
theorem
Submodule.map_equiv_eq_comap_symm
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[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 (↑(LinearEquiv.symm e)) K
theorem
Submodule.comap_equiv_eq_map_symm
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[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 (↑(LinearEquiv.symm e)) K
theorem
Submodule.map_symm_eq_iff
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[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 (LinearEquiv.symm e) K = p ↔ Submodule.map e p = K
theorem
Submodule.orderIsoMapComap_apply'
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[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 (LinearEquiv.symm e) p
theorem
Submodule.orderIsoMapComap_symm_apply'
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[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₂)
:
(OrderIso.symm (Submodule.orderIsoMapComap e)) p = Submodule.map (LinearEquiv.symm e) p
theorem
Submodule.inf_comap_le_comap_add
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[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_10}
{N₂ : Type u_11}
[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_10}
{N₂ : Type u_11}
[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
- One or more equations did not get rendered due to their size.
Instances For
def
LinearMap.submoduleMap
{R : Type u_1}
{M : Type u_6}
{M₁ : Type u_7}
[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
- LinearMap.submoduleMap f p = LinearMap.restrict f (_ : ∀ x ∈ p, f x ∈ Submodule.map f p)
Instances For
@[simp]
theorem
LinearMap.submoduleMap_coe_apply
{R : Type u_1}
{M : Type u_6}
{M₁ : Type u_7}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₁]
[Module R M]
[Module R M₁]
(f : M →ₗ[R] M₁)
{p : Submodule R M}
(x : ↥p)
:
↑((LinearMap.submoduleMap f p) x) = f ↑x
theorem
LinearMap.submoduleMap_surjective
{R : Type u_1}
{M : Type u_6}
{M₁ : Type u_7}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₁]
[Module R M]
[Module R M₁]
(f : M →ₗ[R] M₁)
(p : Submodule R M)
: