Theory Ideal_Extension

section ‹Extension and contraction of ideals along a ring homomorphism›

theory Ideal_Extension
  imports Ideal_Lattice
begin

text ‹Along a homomorphism @{term η} of commutative rings @{text "R → R'"} there are two natural
  operations on ideals:

    ▪ ∗‹contraction› @{text "J ↦ η -` J ∩ R"}, the preimage of an ideal of the target, which is
      always an ideal of the source;

    ▪ ∗‹extension› @{text "I ↦ ⟨η ` I⟩"}, the ideal of the target ∗‹generated by› the image of an
      ideal of the source.  Generation is needed: the direct image @{term "η ` I"} need not be an
      ideal of @{term R'} --- it is closed under addition and under multiplication by elements of
      @{term "η ` R"}, but not in general by arbitrary elements of @{term R'}.  (For the inclusion of the integers in the rationals, the image of the even integers is
      not an ideal of the rationals.)

  These form an ∗‹adjoint pair› between the ideal lattices, ordered by inclusion:
  @{text "⟨η ` I⟩ ⊆ J ⟷ I ⊆ η -` J ∩ R"}.  So this is a genuine instance of the
  @{locale Galois_Connection} locale of ‹Order_Theory›, and all of its consequences --- the unit and
  counit inequalities, monotonicity of both adjoints, the semi-inverse identities, and idempotence of
  the induced closure and kernel operators --- come for free.

  The two rings are commutative because ‹ideal_generated› and ‹ideals› are defined in
  the ‹commutative_ring› context.  As with the module homomorphism locale, the target ring's
  operations are written with primes and the source's unprimed; the two rings are ∗‹separate› here
  (unlike the shared scalar ring of a module homomorphism), so no parameter is shared.›

locale comm_ring_homomorphism = ring_homomorphism +
  source: commutative_ring R "(+)" "(⋅)" 𝟬 𝟭 +
  target: commutative_ring R' "(+')" "(⋅')" "𝟬'" "𝟭'"
begin

subsection ‹Contraction: the preimage of an ideal›

text ‹The contraction of a subset of the target: its preimage, cut down to the source carrier.›
definition contract :: "'b set ⇒ 'a set"
  where "contract J = η -` J ∩ R"

lemma contract_subset: "contract J ⊆ R"
  by (auto simp: contract_def)

lemma contract_memI: "⟦ a ∈ R; η a ∈ J ⟧ ⟹ a ∈ contract J"
  by (simp add: contract_def)

lemma contract_memD: "a ∈ contract J ⟹ a ∈ R ∧ η a ∈ J"
  by (simp add: contract_def)

lemma contract_mono: "J ⊆ J' ⟹ contract J ⊆ contract J'"
  by (auto simp: contract_def)

text ‹The preimage of an ideal is an ideal: it contains the zero because ‹η› preserves it, is closed
  under addition and negation because ‹η› is additive, and absorbs multiplication because ‹η› is
  multiplicative and ‹J› absorbs multiplication in the target.›
theorem contract_ideal:
  assumes J: "Ideal J R' (+') (⋅') 𝟬' 𝟭'"
  shows "Ideal (contract J) R (+) (⋅) 𝟬 𝟭"
proof -
  interpret J: Ideal J R' "(+')" "(⋅')" "𝟬'" "𝟭'" by (rule J)
  ― ‹@{term η} carries the additive inverse to the additive inverse.  This is
    @{thm [source] Monoid_homomorphism.invertible_commutes_with_inverse} for the additive
    homomorphism; its ‹invertible› hypothesis is discharged automatically because the additive
    monoid of a ring is a group.›
  have hom_neg: "η (source.additive.inverse a) = target.additive.inverse (η a)" if a: "a ∈ R" for a
    using a by (simp add: additive.invertible_commutes_with_inverse)
  ― ‹The preimage is an additive subgroup ...›
  have "Subgroup (contract J) R (+) 𝟬"
  proof (rule source.additive.subgroupI)
    show "contract J ⊆ R" by (rule contract_subset)
    show "𝟬 ∈ contract J"
      by (rule contract_memI) (simp_all add: additive.commutes_with_unit J.additive.sub_unit_closed)
    show "⋀g h. ⟦ g ∈ contract J; h ∈ contract J ⟧ ⟹ g + h ∈ contract J"
    proof -
      fix g h assume "g ∈ contract J" and "h ∈ contract J"
      then have gR: "g ∈ R" and hR: "h ∈ R" and hg: "η g ∈ J" and hh: "η h ∈ J"
        by (auto dest: contract_memD)
      have "η (g + h) = η g +' η h"
        using gR hR by (simp add: additive.commutes_with_composition)
      then show "g + h ∈ contract J"
        using gR hR hg hh by (auto intro!: contract_memI J.additive.sub_composition_closed)
    qed
    show "⋀g. g ∈ contract J ⟹ source.additive.invertible g"
      using contract_subset by auto
    show "⋀g. g ∈ contract J ⟹ source.additive.inverse g ∈ contract J"
    proof -
      fix g assume "g ∈ contract J"
      then have gR: "g ∈ R" and hg: "η g ∈ J" by (auto dest: contract_memD)
      have "η (source.additive.inverse g) = target.additive.inverse (η g)"
        using gR by (rule hom_neg)
      moreover have "target.additive.inverse (η g) ∈ J"
        using hg J.additive.sub.invertible by (simp add: J.additive.submonoid_inverse_closed)
      ultimately show "source.additive.inverse g ∈ contract J"
        using gR by (auto intro!: contract_memI)
    qed
  qed
  then interpret S: Subgroup "contract J" R "(+)" 𝟬 .
  ― ‹... and it absorbs multiplication from either side.›
  show ?thesis
  proof unfold_locales
    fix a b assume a: "a ∈ R" and b: "b ∈ contract J"
    then have bR: "b ∈ R" and hb: "η b ∈ J" by (auto dest: contract_memD)
    have "η (a ⋅ b) = η a ⋅' η b"
      using a bR by (simp add: multiplicative.commutes_with_composition)
    also have "… ∈ J" using a hb by (blast intro: J.Ideal(1))
    finally show "a ⋅ b ∈ contract J" using a bR by (blast intro: contract_memI)
  next
    fix a b assume a: "a ∈ R" and b: "b ∈ contract J"
    then have bR: "b ∈ R" and hb: "η b ∈ J" by (auto dest: contract_memD)
    have "η (b ⋅ a) = η b ⋅' η a"
      using a bR by (simp add: multiplicative.commutes_with_composition)
    also have "… ∈ J" using a hb by (blast intro: J.Ideal(2))
    finally show "b ⋅ a ∈ contract J" using a bR by (blast intro: contract_memI)
  qed
qed

text ‹The contraction of the target's zero ideal is the kernel; contracting the whole target gives
  the whole source.›
lemma contract_whole: "contract R' = R"
  using map_closed by (auto simp: contract_def)


subsection ‹Extension: the ideal generated by the image›

text ‹The extension of a subset of the source: the ideal of the target generated by its image.›
definition extend :: "'a set ⇒ 'b set"
  where "extend I = target.ideal_generated (η ` I)"

lemma extend_ideal: "Ideal (extend I) R' (+') (⋅') 𝟬' 𝟭'"
  unfolding extend_def by (rule target.ideal_generated_is_ideal)

lemma extend_subset: "extend I ⊆ R'"
  unfolding extend_def by (rule target.ideal_generated_subset_carrier)

text ‹The image lands inside the extension.  Note the intersection with @{term R'} in
  @{thm [source] target.ideal_generated_incl} is harmless: the image of a subset of @{term R} already
  lies in @{term R'}.›
lemma extend_incl:
  assumes I: "I ⊆ R" shows "η ` I ⊆ extend I"
proof -
  have "η ` I ⊆ R'" using I map_closed by blast
  then have "η ` I ∩ R' = η ` I" by blast
  then show ?thesis
    unfolding extend_def using target.ideal_generated_incl[of "η ` I"] by simp
qed

text ‹Extension is minimal: any target ideal containing the image contains the extension.›
lemma extend_minimal:
  assumes J: "Ideal J R' (+') (⋅') 𝟬' 𝟭'" and sub: "η ` I ⊆ J"
  shows "extend I ⊆ J"
  unfolding extend_def
proof (rule target.ideal_generated_minimal[OF J])
  show "η ` I ∩ R' ⊆ J" using sub by blast
qed

lemma extend_mono:
  assumes II': "I ⊆ I'" and I': "I' ⊆ R" shows "extend I ⊆ extend I'"
proof (rule extend_minimal[OF extend_ideal])
  show "η ` I ⊆ extend I'" using II' extend_incl[OF I'] by blast
qed


subsection ‹The adjunction›

text ‹∗‹Extension is left adjoint to contraction.›  Both directions are immediate from minimality of
  the generated ideal and the definition of preimage --- which is exactly why extension had to be
  defined by generation: without it the left-to-right direction would fail.›
theorem extend_contract_galois:
  assumes I: "I ⊆ R" and J: "Ideal J R' (+') (⋅') 𝟬' 𝟭'"
  shows "extend I ⊆ J ⟷ I ⊆ contract J"
proof
  assume "extend I ⊆ J"
  with extend_incl[OF I] have "η ` I ⊆ J" by blast
  then show "I ⊆ contract J" using I by (auto intro: contract_memI)
next
  assume "I ⊆ contract J"
  then have "η ` I ⊆ J" by (auto dest: contract_memD)
  then show "extend I ⊆ J" by (rule extend_minimal[OF J])
qed

text ‹∗‹The Galois connection.›  On the ideal lattices of the two rings, ordered by inclusion,
  extension and contraction form an adjoint pair.  Interpreting @{locale Galois_Connection} makes its
  whole development available: @{text unit} (@{text "I ⊆ contract (extend I)"}), @{text counit}
  (@{text "extend (contract J) ⊆ J"}), isotonicity of both maps, the semi-inverse laws
  @{text "extend (contract (extend I)) = extend I"} and
  @{text "contract (extend (contract J)) = contract J"}, and idempotence of the closure
  @{text "contract ∘ extend"} and kernel @{text "extend ∘ contract"}.›
theorem ideal_galois_connection:
  "Galois_Connection source.ideals (⊆) target.ideals (⊆) extend contract"
proof (rule Galois_Connection.intro)
  ― ‹Inclusion is a partial order on any set of sets; ‹Ideal_Lattice›'s own interpretation is
    inside its ‹commutative_ring› context and so is not citable by name from here.›
  show "Partial_Order source.ideals (⊆)" by unfold_locales auto
  show "Partial_Order target.ideals (⊆)" by unfold_locales auto
  show "Galois_Connection_axioms source.ideals (⊆) target.ideals (⊆) extend contract"
  proof
    show "extend ∈ source.ideals → target.ideals"
      using extend_ideal by (auto simp: target.ideals_iff)
    show "contract ∈ target.ideals → source.ideals"
      using contract_ideal by (auto simp: source.ideals_iff target.ideals_iff)
    fix I J assume "I ∈ source.ideals" and "J ∈ target.ideals"
    then have I: "Ideal I R (+) (⋅) 𝟬 𝟭" and J: "Ideal J R' (+') (⋅') 𝟬' 𝟭'"
      by (simp_all add: source.ideals_iff target.ideals_iff)
    interpret I: Ideal I R "(+)" "(⋅)" 𝟬 𝟭 by (rule I)
    have IR: "I ⊆ R" by (rule I.additive.subset)
    show "extend I ⊆ J ⟷ I ⊆ contract J" by (rule extend_contract_galois[OF IR J])
  qed
qed

text ‹The consequences of the adjunction, specialised to ideals.  These are obtained by interpreting
  @{thm [source] ideal_galois_connection} locally rather than by a @{command sublocale} declaration:
  a ‹sublocale galois_connection› inside this locale sends the interpretation machinery into a loop,
  because @{locale comm_ring_homomorphism} would then be a source of ‹galois_connection› facts about
  its own ideal lattices while still being elaborated.  The theorem form has no such problem, and
  consumers can ⬚‹interpret› it wherever they need the full development.›

context
begin

interpretation GC: Galois_Connection
  "source.ideals" "(⊆)" "target.ideals" "(⊆)" extend contract
  by (rule ideal_galois_connection)

text ‹∗‹Unit›: an ideal is contained in the contraction of its extension.›
corollary contract_extend_incl:
  "Ideal I R (+) (⋅) 𝟬 𝟭 ⟹ I ⊆ contract (extend I)"
  using GC.unit by simp

text ‹∗‹Counit›: the extension of a contraction is contained in the original ideal.  The inclusion is
  in general strict --- for @{text "ℤ ⊆ ℚ"} every nonzero ideal of @{text ℚ} contracts to a
  nonzero ideal of @{text ℤ} whose extension is all of @{text ℚ}.›
corollary extend_contract_subset:
  "Ideal J R' (+') (⋅') 𝟬' 𝟭' ⟹ extend (contract J) ⊆ J"
  using GC.counit by simp

text ‹Both adjoints are isotone on ideals.›
corollary extend_mono_ideal:
  "⟦ Ideal I R (+) (⋅) 𝟬 𝟭; Ideal I' R (+) (⋅) 𝟬 𝟭; I ⊆ I' ⟧ ⟹ extend I ⊆ extend I'"
  using isotone_le[OF GC.lower_isotone] by simp

corollary contract_mono_ideal:
  "⟦ Ideal J R' (+') (⋅') 𝟬' 𝟭'; Ideal J' R' (+') (⋅') 𝟬' 𝟭'; J ⊆ J' ⟧
   ⟹ contract J ⊆ contract J'"
  using isotone_le[OF GC.upper_isotone] by simp

text ‹The ∗‹semi-inverse› laws: extension and contraction are mutually inverse up to one round trip.›
corollary extend_contract_extend:
  "Ideal I R (+) (⋅) 𝟬 𝟭 ⟹ extend (contract (extend I)) = extend I"
  using GC.lower_semi_inverse by simp

corollary contract_extend_contract:
  "Ideal J R' (+') (⋅') 𝟬' 𝟭' ⟹ contract (extend (contract J)) = contract J"
  using GC.upper_semi_inverse by simp

text ‹Hence @{text "contract ∘ extend"} is a closure operator on the ideals of the source, and
  @{text "extend ∘ contract"} a kernel operator on those of the target.›
corollary closure_idempotent:
  "Ideal I R (+) (⋅) 𝟬 𝟭 ⟹ contract (extend (contract (extend I))) = contract (extend I)"
  using GC.closure_idempotent by simp

corollary kernel_idempotent:
  "Ideal J R' (+') (⋅') 𝟬' 𝟭' ⟹ extend (contract (extend (contract J))) = extend (contract J)"
  using GC.kernel_idempotent by simp

end

end (* comm_ring_homomorphism *)

end