English
Characterization of coeSubmodule membership: y ∈ coeSubmodule L (conductor R x) iff ∀ z ∈ S, y (algebraMap_S L z) ∈ adjoin_R{algebraMap_S L x}.
Русский
Характеризация принадлежности к coeSubmodule: y ∈ coeSubmodule L (conductor R x) тогда и только если ∀ z ∈ S, y·algebraMap_S L z ∈ adjoin_R{algebraMap_S L x}.
LaTeX
$$$y \\in \\mathrm{coeSubmodule}\\, L\\, (\\mathrm{conductor}(R,x)) \\iff \\forall z \\in S,\\ y \\cdot (\\mathrm{algebraMap}_S L z) \\in \\mathrm{adjoin}_R\\{\\mathrm{algebraMap}_S L x\\}$$$
Lean4
theorem mem_coeSubmodule_conductor {L} [CommRing L] [Algebra S L] [Algebra R L] [IsScalarTower R S L]
[NoZeroSMulDivisors S L] {x : S} {y : L} :
y ∈ coeSubmodule L (conductor R x) ↔ ∀ z : S, y * (algebraMap S L) z ∈ Algebra.adjoin R {algebraMap S L x} :=
by
cases subsingleton_or_nontrivial L
· rw [Subsingleton.elim (coeSubmodule L _) ⊤, Subsingleton.elim (Algebra.adjoin R _) ⊤]; simp
trans ∀ z, y * (algebraMap S L) z ∈ (Algebra.adjoin R { x }).map (IsScalarTower.toAlgHom R S L)
· simp only [coeSubmodule, Submodule.mem_map, Algebra.linearMap_apply, Subalgebra.mem_map,
IsScalarTower.coe_toAlgHom']
constructor
· rintro ⟨y, hy, rfl⟩ z
exact ⟨_, hy z, map_mul _ _ _⟩
· intro H
obtain ⟨y, _, e⟩ := H 1
rw [map_one, mul_one] at e
subst e
simp only [← map_mul, (FaithfulSMul.algebraMap_injective S L).eq_iff, exists_eq_right] at H
exact ⟨_, H, rfl⟩
· rw [AlgHom.map_adjoin, Set.image_singleton]; rfl
