index_smul_le — Mathlib

English

Let I be an ideal, N ⊆ M a submodule with generators s, such that N = span(s). If R/I is finite, then the index [M: I·N] is bounded by [R:I]^{|s|} [M:N].

Русский

Пусть I — идеал, N — подмодуль, порожденный множеством s, и R/I конечно. Тогда индекс [M: I·N] ограничен сверху как [R:I]^{|s|} [M:N].

LaTeX

$$$$[M: I\cdot N] \le [R:I]^{|s|}\cdot [M:N].$$$$

Lean4

theorem index_smul_le [Finite (R ⧸ I)] (s : Finset M) (hs : Submodule.span R s = N) :
    (I • N).toAddSubgroup.index ≤ I.toAddSubgroup.index ^ s.card * N.toAddSubgroup.index := by
  classical
  cases nonempty_fintype (R ⧸ I)
  rw [← AddSubgroup.relIndex_mul_index (H := (I • N).toAddSubgroup) (K := N.toAddSubgroup) Submodule.smul_le_right]
  gcongr
  change (Nat.card (N ⧸ (I • N).comap N.subtype)) ≤ Nat.card (R ⧸ I) ^ s.card
  let e : (N ⧸ (I • N).comap N.subtype) ≃ₗ[R] (R ⧸ I) ⊗[R] N :=
    Submodule.quotEquivOfEq _ (I • (⊤ : Submodule R N))
        (Submodule.map_injective_of_injective N.injective_subtype (by simp [Submodule.smul_le_right])) ≪≫ₗ
      (quotTensorEquivQuotSMul N I).symm
  rw [Nat.card_congr e.toEquiv]
  have H : LinearMap.range (Finsupp.linearCombination R (α := s) (↑)) = N := by
    rw [Finsupp.range_linearCombination, ← hs, Subtype.range_val]; rfl
  let f : (s →₀ R) →ₗ[R] N :=
    (Finsupp.linearCombination R (↑)).codRestrict _
      (fun c => by rw [← H, LinearMap.mem_range]; exact exists_apply_eq_apply _ _)
  have hf : Function.Surjective f := fun x ↦ by obtain ⟨y, hy⟩ := H.ge x.2; exact ⟨y, Subtype.ext hy⟩
  have : Function.Surjective (f.lTensor (R ⧸ I) ∘ₗ (finsuppScalarRight R (R ⧸ I) s).symm.toLinearMap) :=
    (LinearMap.lTensor_surjective (R ⧸ I) hf).comp (LinearEquiv.surjective _)
  refine (Nat.card_le_card_of_surjective _ this).trans ?_
  simp only [Nat.card_eq_fintype_card, Fintype.card_finsupp, Fintype.card_coe, le_rfl]

Похожие утверждения