LeanPool.BruhatTits.Utils.LinearAlgebra

theorem Submodule.zero_lt_finrank_of_ne_bot {R : Type u_1} {M : Type u_2} [Field R] [AddCommGroup M] [Module R M] [Module.Finite R M] (p : Submodule R M) (hp : p ≠ ⊥) : 0 < Module.finrank R ↥p

theorem Submodule.finrank_lt_finrank_of_ne_top {R : Type u_1} {M : Type u_2} [Field R] [AddCommGroup M] [Module R M] [Module.Finite R M] (p : Submodule R M) (hp : p ≠ ⊤) : Module.finrank R ↥p < Module.finrank R M

theorem Submodule.exists_generator_of_finrank_eq_one {R : Type u_1} {M : Type u_2} [Field R] [AddCommGroup M] [Module R M] [Module.Finite R M] (p : Submodule R M) (h : Module.finrank R ↥p = 1) : ∃ (v : M), v ≠ 0 ∧ R ∙ v = p

theorem Submodule.exists_generator_of_finrank_eq_one_basis {R : Type u_1} {M : Type u_2} [Field R] [AddCommGroup M] [Module R M] [Module.Finite R M] (b : Module.Basis (Fin 2) R M) (p : Submodule R M) (hr : Module.finrank R ↥p = 1) (ht : p ≠ R ∙ b 0) : ∃ (a : R), p = R ∙ (a • b 0 + b 1)

noncomputable def quotTensorEquivQuotSMul' {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] (I : Ideal R) : TensorProduct R (R ⧸ I) M ≃ₗ[R ⧸ I] M ⧸ I • ⊤

As a module of the quotient ring, left tensoring a module with a quotient of the ring is the same as quotienting that module by the corresponding submodule.

Equations

• quotTensorEquivQuotSMul' M I = LinearEquiv.extendScalarsOfSurjective ⋯ (TensorProduct.quotTensorEquivQuotSMul M I)

noncomputable def TensorProduct.quotientEquivPiOfBasis {R : Type u_5} {M : Type u_6} [CommRing R] (I : Ideal R) [AddCommGroup M] [Module R M] {ι : Type u_7} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R M) : (M ⧸ I • ⊤) ≃ₗ[R ⧸ I] ι → R ⧸ I

If b is an ι-indexed basis of M and Ìis an ideal ofR, the quotient M ⧸ I MisR ⧸ Iisomorphic toι → R ⧸ I`.

Equations

• One or more equations did not get rendered due to their size.

theorem quotient_finrank_eq {R : Type u_5} {M : Type u_6} [CommRing R] (I : Ideal R) [AddCommGroup M] [Module R M] {ι : Type u_7} [Fintype ι] [StrongRankCondition (R ⧸ I)] (b : Module.Basis ι R M) : Module.finrank (R ⧸ I) (M ⧸ I • ⊤) = Fintype.card ι

If M is free, the rank of M ⧸ IMas an R ⧸ I-module is the rank of M as an R-module.

Order on submodule above a fixed submodule

@[implicit_reducible]

instance instOrderTopSubtypeSubmoduleLeLeanPool {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : OrderTop { p' : Submodule R M // p ≤ p' }

Equations

• instOrderTopSubtypeSubmoduleLeLeanPool p = { top := ⟨⊤, ⋯⟩, le_top := ⋯ }

@[implicit_reducible]

instance instOrderBotSubtypeSubmoduleLeLeanPool {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : OrderBot { p' : Submodule R M // p ≤ p' }

Equations

• instOrderBotSubtypeSubmoduleLeLeanPool p = { bot := ⟨p, ⋯⟩, bot_le := ⋯ }

theorem Submodule.quotient_equiv_eq_bot_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (p' : { p' : Submodule R M // p ≤ p' }) : p' = ⊥ ↔ ↑p' = p

theorem lt_of_ne_top {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) {p' : Submodule R ↥p} (q : { q : Submodule R ↥p // p' ≤ q }) (h : q ≠ ⊤) : Submodule.map p.subtype ↑q < p

@[simp]

theorem Submodule.comap_subtype_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (p : Submodule R M) : comap p.subtype (I • p) = I • ⊤

theorem Submodule.map_subtype_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (p : Submodule R M) : map p.subtype (I • ⊤) = I • p

theorem ideal_smul_lt_of_ne_bot {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (p : Submodule R M) (q : { q : Submodule R ↥p // I • ⊤ ≤ q }) (h : q ≠ ⊥) : I • p < Submodule.map p.subtype ↑q

@[simp]

theorem Matrix.GeneralLinearGroup.toLin_symm_apply {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommRing R] (g : LinearMap.GeneralLinearGroup R (n → R)) (x : n → R) : (↑(toLin.symm g)).mulVec x = ↑g x