map_includeRight_eq — Mathlib

English

For an ideal I of B, the ideal in A ⊗ B generated by I is the image of A ⊗ I under the right include map.

Русский

Для идеала I в B, порожденный в A ⊗ B равен образу A ⊗ I под правым включением.

LaTeX

$$$(I.map(\\mathrm{Algebra.TensorProduct.includeRight} : B \\to_A[R] A \\otimes_R B)).restrictScalars R = \\mathrm{range}(\\mathrm{lTensor} A\\,(\\mathrm{subtype} (I\\restriction_R)))$$$

Lean4

/-- The ideal of `A ⊗[R] B` generated by `I` is the image of `A ⊗[R] I` -/
theorem map_includeRight_eq (I : Ideal B) :
    (I.map (Algebra.TensorProduct.includeRight : B →ₐ[R] A ⊗[R] B)).restrictScalars R =
      LinearMap.range (LinearMap.lTensor A (Submodule.subtype (I.restrictScalars R))) :=
  by
  rw [← SetLike.coe_set_eq]
  apply le_antisymm
  · intro x hx
    simp only [SetLike.mem_coe, LinearMap.mem_range]
    rw [Ideal.map, ← submodule_span_eq] at hx
    refine Submodule.span_induction ?_ ?_ ?_ ?_ hx
    · intro x
      simp only [includeRight_apply, Set.mem_image, SetLike.mem_coe]
      rintro ⟨y, hy, rfl⟩
      use 1 ⊗ₜ[R] ⟨y, hy⟩
      rfl
    · use 0
      simp only [map_zero]
    · rintro x y - - ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩
      use x + y
      simp only [map_add]
    · rintro a x - ⟨x, hx, rfl⟩
      induction a with
      | zero =>
        use 0
        simp only [map_zero, smul_eq_mul, zero_mul]
      | tmul a b =>
        induction x with
        | zero =>
          use 0
          simp only [map_zero, smul_eq_mul, mul_zero]
        | tmul x y =>
          use (a * x) ⊗ₜ[R] (b • y)
          simp only [LinearMap.lTensor_tmul, Submodule.coe_subtype, smul_eq_mul, tmul_mul_tmul]
          rfl
        | add x y hx hy =>
          obtain ⟨x', hx'⟩ := hx
          obtain ⟨y', hy'⟩ := hy
          use x' + y'
          simp only [map_add, hx', smul_add, hy']
      | add a b ha hb =>
        obtain ⟨x', ha'⟩ := ha
        obtain ⟨y', hb'⟩ := hb
        use x' + y'
        simp only [map_add, ha', add_smul, hb']
  · rintro x ⟨y, rfl⟩
    induction y with
    | zero =>
      rw [map_zero]
      apply zero_mem
    | tmul a b =>
      simp only [LinearMap.lTensor_tmul, Submodule.coe_subtype]
      suffices a ⊗ₜ[R] (b : B) = (a ⊗ₜ[R] (1 : B)) * ((1 : A) ⊗ₜ[R] (b : B))
        by
        rw [this]
        simp only [Submodule.coe_restrictScalars, SetLike.mem_coe]
        apply Ideal.mul_mem_left
        apply Ideal.mem_map_of_mem includeRight
        exact Submodule.coe_mem b
      simp only [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]
    | add x y hx hy =>
      rw [map_add]
      apply Submodule.add_mem _ hx hy

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