Grace/Cumulus/Algebra/Field/Quotient.g17

Open in Workbench Download source

Imports

Construction · Ring.Quotient · Ring.IdealAdjoin

Declarations

Source

1-- Maximal ideals and quotient fields, with canonical inverses in ZF.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Field.Quotient8import Construction9import Ring.Quotient10import Ring.IdealAdjoin1112theorem IsMaximalIdeal.unit_modulo (A add zero neg mul one I x : Set)13  requires ring : IsCommRing(A, add, zero, neg, mul, one)14  requires maximal : IsMaximalIdeal(A, add, zero, neg, mul, one, I)15  requires hx : x ∈ A16  requires outside : ¬(x ∈ I)17  shows ∃ a ∈ A, Congruent(add, neg, I, call2(mul, a, x), one)18proof19  have ideal : IsIdeal(A, add, zero, neg, mul, I) by simp [IsMaximalIdeal, IsProperIdeal]20  have bounded := IsIdeal.subset_carrier with ideal21  obtain ⟨i, hi, a, ha, equation⟩ := IsMaximalIdeal.bezout at A, add, zero, neg, mul, one, I, x with *22  have iInA := bounded with i, hi23  have negative := IsIdeal.neg_closed with *24  have difference : call2(add, call2(mul, a, x), neg(one)) = neg(i)25    rw equation26    ring27  refine ⟨a, ha, ?_⟩28  unfold Congruent29  rwa difference3031theorem idealQuotient.is_field_of_maximal (A add zero neg mul one I : Set)32  requires ring : IsCommRing(A, add, zero, neg, mul, one)33  requires maximal : IsMaximalIdeal(A, add, zero, neg, mul, one, I)34  shows IsField((A ⧸ idealRelation(A, add, neg, I)),35    quotientBinary(A, idealRelation(A, add, neg, I), add), ⟦zero⟧[A, idealRelation(A, add, neg, I)],36    quotientUnary(A, idealRelation(A, add, neg, I), neg), quotientBinary(A, idealRelation(A, add, neg, I), mul), ⟦one⟧[A, idealRelation(A, add, neg, I)])37proof38  have proper : IsProperIdeal(A, add, zero, neg, mul, one, I) by simp [IsMaximalIdeal]39  have ideal : IsIdeal(A, add, zero, neg, mul, I) by simp [IsProperIdeal]40  have ordinary := IsCommRing.ring with ring41  have monoid := IsRing.multiplicative with ordinary42  have oneInA := IsMonoid.unit_in_carrier with monoid43  have closed : IsMagma(A, mul) by simp [IsMonoid, IsSemigroup]44  have equivalence := idealRelation.equivalence with *45  have compatible := idealRelation.mul_compatible with *46  have quotientRing := idealQuotient.comm_ring with *47  have nontrivial := idealQuotient.nontrivial_iff.backward with ring, ideal, proper48  unfold IsField49  refine ⟨quotientRing, nontrivial, ?_⟩50  intros X hX nonzero51  obtain ⟨x, hx, shape⟩ := quotient.representative with hX52  have outside : ¬(x ∈ I)53    intro member54    have equal := idealClass.eq_zero.backward with ring, ideal, hx, member55    apply nonzero56    cc57  obtain ⟨a, ha, congruence⟩ := IsMaximalIdeal.unit_modulo at A, add, zero, neg, mul, one, I, x with *58  have productInA := IsRing.mul_closed with ha, hx59  have equal := idealClass.eq_iff_congruent.backward with ring, ideal, productInA, oneInA, congruence60  have aIn := quotient.contains_class with ha61  have left := quotientBinary.classes with ha, hx62  have right := quotientBinary.classes with hx, ha63  have commutes := IsCommRing.mul_comm with hx, ha64  witness ⟦a⟧[A, idealRelation(A, add, neg, I)]65  unfold IsInverse66  refine ⟨hX, ⟨aIn, ⟨?_, ?_⟩⟩⟩67  . cc68  . cc6970theorem idealQuotient.maximal_of_is_field (A add zero neg mul one I : Set)71  requires ring : IsCommRing(A, add, zero, neg, mul, one)72  requires ideal : IsIdeal(A, add, zero, neg, mul, I)73  requires field : IsField((A ⧸ idealRelation(A, add, neg, I)),74    quotientBinary(A, idealRelation(A, add, neg, I), add), ⟦zero⟧[A, idealRelation(A, add, neg, I)],75    quotientUnary(A, idealRelation(A, add, neg, I), neg), quotientBinary(A, idealRelation(A, add, neg, I), mul), ⟦one⟧[A, idealRelation(A, add, neg, I)])76  shows IsMaximalIdeal(A, add, zero, neg, mul, one, I)77proof78  have nontrivial := IsField.nontrivial with field79  have proper := idealQuotient.nontrivial_iff.forward with *80  have ordinary := IsCommRing.ring with ring81  have monoid := IsRing.multiplicative with ordinary82  have oneInA := IsMonoid.unit_in_carrier with monoid83  have closed : IsMagma(A, mul) by simp [IsMonoid, IsSemigroup]84  have equivalence := idealRelation.equivalence with *85  have compatible := idealRelation.mul_compatible with *86  unfold IsMaximalIdeal87  refine ⟨proper, ?_⟩88  intros J properJ contains89  have idealJ : IsIdeal(A, add, zero, neg, mul, J) by simp [IsProperIdeal]90  have boundedJ := IsIdeal.subset_carrier with idealJ91  apply Subset.antisymmetric92    intros x hx93    have xInA := boundedJ with x, hx94    by_contra outside95    have xClassIn := quotient.contains_class at A, idealRelation(A, add, neg, I), x with *96    have nonzero : ⟦x⟧[A, idealRelation(A, add, neg, I)] ≠ ⟦zero⟧[A, idealRelation(A, add, neg, I)]97      intro equal98      have member := idealClass.eq_zero.forward with ring, ideal, xInA, equal99      exact outside with member100    obtain ⟨Y, inverse⟩ := IsField.inverse_exists with field, xClassIn, nonzero101    have yClassIn := inverse.right.left102    obtain ⟨y, hy, shape⟩ := quotient.representative with yClassIn103    have left := inverse.right.right.left104    have multiply := quotientBinary.classes at A, idealRelation(A, add, neg, I), mul, y, x with *105    have equal : ⟦call2(mul, y, x)⟧[A, idealRelation(A, add, neg, I)] = ⟦one⟧[A, idealRelation(A, add, neg, I)] by cc106    have productInA := IsRing.mul_closed at A, add, zero, neg, mul, one, y, x with *107    have congruence := idealClass.eq_iff_congruent.forward with ring, ideal, productInA, oneInA, equal108    have differenceInJ : call2(add, call2(mul, y, x), neg(one)) ∈ J109      exact contains with call2(add, call2(mul, y, x), neg(one)), congruence110    have productInJ := IsIdeal.mul_left_closed with hy, hx111    have negative := IsIdeal.neg_closed at A, add, zero, neg, mul, J, call2(add, call2(mul, y, x), neg(one)) with *112    have sum := IsIdeal.add_closed at A, add, zero, neg, mul, J, call2(mul, y, x), neg(call2(add, call2(mul, y, x), neg(one))) with *113    have oneInJ : one ∈ J114      ring_nf at sum115      exact sum116    exact properJ.right with oneInJ117  . exact contains118119theorem idealQuotient.is_field_iff_maximal (A add zero neg mul one I : Set)120  requires ring : IsCommRing(A, add, zero, neg, mul, one)121  requires ideal : IsIdeal(A, add, zero, neg, mul, I)122  shows IsField((A ⧸ idealRelation(A, add, neg, I)),123    quotientBinary(A, idealRelation(A, add, neg, I), add), ⟦zero⟧[A, idealRelation(A, add, neg, I)],124    quotientUnary(A, idealRelation(A, add, neg, I), neg), quotientBinary(A, idealRelation(A, add, neg, I), mul), ⟦one⟧[A, idealRelation(A, add, neg, I)]) ↔ IsMaximalIdeal(A, add, zero, neg, mul, one, I)125proof126  constructor127  . intro field128    exact idealQuotient.maximal_of_is_field with *129  . intro maximal130    exact idealQuotient.is_field_of_maximal with *131132def idealQuotientInverse (A add zero neg mul one I : Set) : Set :=133  fieldInverse((A ⧸ idealRelation(A, add, neg, I)),134    quotientBinary(A, idealRelation(A, add, neg, I), add), ⟦zero⟧[A, idealRelation(A, add, neg, I)],135    quotientUnary(A, idealRelation(A, add, neg, I), neg), quotientBinary(A, idealRelation(A, add, neg, I), mul), ⟦one⟧[A, idealRelation(A, add, neg, I)])136137theorem idealQuotient.field_of_maximal (A add zero neg mul one I : Set)138  requires ring : IsCommRing(A, add, zero, neg, mul, one)139  requires maximal : IsMaximalIdeal(A, add, zero, neg, mul, one, I)140  shows IsFieldWithInverse((A ⧸ idealRelation(A, add, neg, I)),141    quotientBinary(A, idealRelation(A, add, neg, I), add), ⟦zero⟧[A, idealRelation(A, add, neg, I)],142    quotientUnary(A, idealRelation(A, add, neg, I), neg), quotientBinary(A, idealRelation(A, add, neg, I), mul), ⟦one⟧[A, idealRelation(A, add, neg, I)],143    idealQuotientInverse(A, add, zero, neg, mul, one, I))144proof145  have structure := idealQuotient.is_field_of_maximal with *146  have field := IsField.field with structure147  unfold idealQuotientInverse148  exact field149