Theory Subring_Generated

section ‹The subring generated by a set›

theory Subring_Generated
  imports Ring_Theory
begin

text ‹Mirroring the subgroup ‹generate› and the ideal generated by a set, the subring generated by
  a subset ‹S› of a ring is the intersection of all subrings containing ‹S ∩ R›.  We first show
  that an intersection of a nonempty family of subrings is a subring; the whole ring is a subring
  of itself, so the family intersected is always nonempty.›

context Ring
begin

subsection ‹Intersections of subrings›

text ‹The intersection of a nonempty family of subrings is a subring.›
lemma subring_Inter:
  assumes ne: "𝒜 ≠ {}" and sr: "⋀S. S ∈ 𝒜 ⟹ Subring S R (+) (⋅) 𝟬 𝟭"
  shows "Subring (⋂ 𝒜) R (+) (⋅) 𝟬 𝟭"
proof -
  obtain S0 where S0: "S0 ∈ 𝒜" using ne by blast
  interpret S0: Subring S0 R "(+)" "(⋅)" 𝟬 𝟭 by (rule sr[OF S0])
  ― ‹The additive part is a subgroup.›
  have sg: "Subgroup (⋂ 𝒜) R (+) 𝟬"
  proof (rule additive.subgroupI)
    show "⋂ 𝒜 ⊆ R" using S0 S0.additive.subset by blast
  next
    show "𝟬 ∈ ⋂ 𝒜"
    proof
      fix S assume "S ∈ 𝒜"
      then interpret S: Subring S R "(+)" "(⋅)" 𝟬 𝟭 by (rule sr)
      show "𝟬 ∈ S" by (rule S.additive.sub_unit_closed)
    qed
  next
    fix g h assume g: "g ∈ ⋂ 𝒜" and h: "h ∈ ⋂ 𝒜"
    show "g + h ∈ ⋂ 𝒜"
    proof
      fix S assume S: "S ∈ 𝒜"
      then interpret S: Subring S R "(+)" "(⋅)" 𝟬 𝟭 by (rule sr)
      show "g + h ∈ S" using g h S by (blast intro: S.additive.sub_composition_closed)
    qed
  next
    fix g assume "g ∈ ⋂ 𝒜"
    then have "g ∈ R" using S0 S0.additive.subset by blast
    then show "additive.invertible g" by simp
  next
    fix g assume g: "g ∈ ⋂ 𝒜"
    show "additive.inverse g ∈ ⋂ 𝒜"
    proof
      fix S assume S: "S ∈ 𝒜"
      then interpret S: Subring S R "(+)" "(⋅)" 𝟬 𝟭 by (rule sr)
      have "g ∈ S" using g S by blast
      then show "additive.inverse g ∈ S"
        using S.additive.submonoid_inverse_closed S.additive.sub.invertible by blast
    qed
  qed
  ― ‹The multiplicative part is a submonoid.›
  interpret sg: Subgroup "⋂ 𝒜" R "(+)" 𝟬 by (rule sg)
  show ?thesis
  proof
    show "⋂ 𝒜 ⊆ R" using sg.subset .
    show "𝟭 ∈ ⋂ 𝒜"
    proof
      fix S assume "S ∈ 𝒜"
      then interpret S: Subring S R "(+)" "(⋅)" 𝟬 𝟭 by (rule sr)
      show "𝟭 ∈ S" by (rule S.multiplicative.sub_unit_closed)
    qed
    fix a b assume a: "a ∈ ⋂ 𝒜" and b: "b ∈ ⋂ 𝒜"
    show "a ⋅ b ∈ ⋂ 𝒜"
    proof
      fix S assume S: "S ∈ 𝒜"
      then interpret S: Subring S R "(+)" "(⋅)" 𝟬 𝟭 by (rule sr)
      show "a ⋅ b ∈ S" using a b S by (blast intro: S.multiplicative.sub_composition_closed)
    qed
  qed
qed


text ‹The whole ring is a subring of itself (the top subring).›
lemma whole_subring: "Subring R R (+) (⋅) 𝟬 𝟭"
proof -
  have "Subgroup R R (+) 𝟬" by (rule additive.subgroupI) auto
  then interpret sg: Subgroup R R "(+)" 𝟬 .
  show ?thesis by unfold_locales auto
qed


subsection ‹The generated subring›

text ‹The subring generated by a subset ‹S›: the intersection of all subrings containing
  ‹S ∩ R› (intersecting with ‹R› in the guard, as with subgroups and ideals, so that elements
  outside the carrier are ignored).›
definition subring_generated :: "'a set ⇒ 'a set"
  where "subring_generated S = ⋂ {T. Subring T R (+) (⋅) 𝟬 𝟭 ∧ S ∩ R ⊆ T}"

lemma subring_generated_is_subring: "Subring (subring_generated S) R (+) (⋅) 𝟬 𝟭"
proof -
  have "R ∈ {T. Subring T R (+) (⋅) 𝟬 𝟭 ∧ S ∩ R ⊆ T}" using whole_subring by auto
  then have ne: "{T. Subring T R (+) (⋅) 𝟬 𝟭 ∧ S ∩ R ⊆ T} ≠ {}" by blast
  show ?thesis
    unfolding subring_generated_def by (rule subring_Inter[OF ne]) auto
qed

lemma subring_generated_incl: "S ∩ R ⊆ subring_generated S"
  unfolding subring_generated_def by blast

lemma subring_generated_minimal:
  assumes "Subring T R (+) (⋅) 𝟬 𝟭" "S ∩ R ⊆ T"
  shows "subring_generated S ⊆ T"
  unfolding subring_generated_def using assms by (blast intro: Inter_lower)

lemma subring_generated_subset_carrier: "subring_generated S ⊆ R"
proof -
  interpret gen: Subring "subring_generated S" R "(+)" "(⋅)" 𝟬 𝟭
    by (rule subring_generated_is_subring)
  show ?thesis by (rule gen.additive.subset)
qed

end

end